--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 07 14:05:32 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 07 14:05:33 2013 +0100
@@ -145,7 +145,7 @@
fun ext_name ctxt =
if Thm.eq_thm_prop (@{thm ext},
- singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
+ singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
isa_short_ext
else
isa_ext
@@ -158,8 +158,8 @@
insert (op =) (ext_name ctxt, (Global, General))
else if rule = leo2_unfold_def_rule then
(* LEO 1.3.3 does not record definitions properly, leading to missing
- dependencies in the TSTP proof. Remove the next line once this is
- fixed. *)
+ dependencies in the TSTP proof. Remove the next line once this is
+ fixed. *)
add_non_rec_defs fact_names
else if rule = satallax_coreN then
(fn [] =>
@@ -169,8 +169,7 @@
| facts => facts)
else
I)
- #> (if null deps then union (op =) (resolve_fact fact_names ss)
- else I)
+ #> (if null deps then union (op =) (resolve_fact fact_names ss) else I)
| add_fact _ _ _ = I
fun used_facts_in_atp_proof ctxt fact_names atp_proof =