# HG changeset patch
# User blanchet
# Date 1360242333 -3600
# Node ID 48e82e199df16f93d0b5f54293b55dd33fb93a68
# Parent  4acc150a321ae835a5cd27ce7c3265400c8fe8ef
tuned indent

diff -r 4acc150a321a -r 48e82e199df1 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- 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 []
diff -r 4acc150a321a -r 48e82e199df1 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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 =