# HG changeset patch
# User blanchet
# Date 1357138953 -3600
# Node ID 70a1c2731ab69484c9f6aa58f719e0f6c25b70a8
# Parent  f1426d48942f4f854f721c747a3d05547d85859b
tuning

diff -r f1426d48942f -r 70a1c2731ab6 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Jan 02 15:54:38 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Jan 02 16:02:33 2013 +0100
@@ -702,12 +702,11 @@
         fun maybe_show outer c =
           (outer andalso length c = 1 andalso subset (op =) (c, conjs))
           ? cons Show
-        fun do_have outer qs (gamma, c) =
-          Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c,
-                 By_Metis (fold (add_fact_from_dependencies fact_names) gamma
-                                ([], [])))
-        fun do_inf outer (Have z) = do_have outer [] z
-          | do_inf outer (Cases cases) =
+        fun isar_step_of_direct_inf outer (Have (gamma, c)) =
+            Prove (maybe_show outer c [], label_of_clause c, prop_of_clause c,
+                   By_Metis (fold (add_fact_from_dependencies fact_names) gamma
+                                  ([], [])))
+          | isar_step_of_direct_inf outer (Cases cases) =
             let val c = succedent_of_cases cases in
               Prove (maybe_show outer c [Ultimately], label_of_clause c,
                      prop_of_clause c,
@@ -715,11 +714,11 @@
             end
         and do_case outer (c, infs) =
           Assume (label_of_clause c, prop_of_clause c) ::
-          map (do_inf outer) infs
+          map (isar_step_of_direct_inf outer) infs
         val (isar_proof, (preplay_fail, ext_time)) =
           ref_graph
           |> redirect_graph axioms tainted
-          |> map (do_inf true)
+          |> map (isar_step_of_direct_inf true)
           |> append assms
           |> (if not preplay andalso isar_shrink <= 1.0 then
                 pair (false, (true, seconds 0.0)) #> swap