@@ -181,7+181,9 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
| _ -> p.Con.proof_context)
presacontext
in
| _ -> p.Con.proof_context)
presacontext
in
+(*
let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (if is_top_down then "(TD)" else "(NTD)") ^ "*)"); body; B.b_kw "(*>>*)"]) in
let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (if is_top_down then "(TD)" else "(NTD)") ^ "*)"); body; B.b_kw "(*>>*)"]) in
+*)
match p.Con.proof_name with
None -> body
| Some name ->
match p.Con.proof_name with
None -> body
| Some name ->
@@ -447,9+449,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (
| Some j -> [j]
in
let index_term1, index_term2 =
| Some j -> [j]
in
let index_term1, index_term2 =
- if (conclude.Con.conclude_method = "RewriteLR" && is_top_down)
- || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down)
- then 2,5 else 5,2
+ if conclude.Con.conclude_method = "RewriteLR" then 2,5 else 5,2
in
let term1 =
(match List.nth conclude.Con.conclude_args index_term1 with
in
let term1 =
(match List.nth conclude.Con.conclude_args index_term1 with