--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Thu Feb 07 14:05:32 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Thu Feb 07 14:05:33 2013 +0100
@@ -498,10 +498,10 @@
|> chop special_fact_index
in bef @ add @ after end
fun insert_special_facts accepts =
- (* FIXME: get rid of "ext" here once it is treated as a helper *)
- [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
- |> add_set_const_thms accepts
- |> insert_into_facts accepts
+ (* FIXME: get rid of "ext" here once it is treated as a helper *)
+ [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
+ |> add_set_const_thms accepts
+ |> insert_into_facts accepts
in
facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
|> iter 0 max_facts thres0 goal_const_tab []
--- 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 =