# HG changeset patch
# User blanchet
# Date 1391190196 -3600
# Node ID 70035950e19bb61462674d800522597daf0bea8c
# Parent  77953325d5f1ff07a359471fbddc6abe524ab01e
tuning

diff -r 77953325d5f1 -r 70035950e19b src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
@@ -235,12 +235,6 @@
 
     fun add_assms ind assms = fold (add_assm ind) assms
 
-    fun add_step_post ind l t (ls, ss) meth =
-      add_str (of_label l)
-      #> add_term t
-      #> add_str (" " ^
-           of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^ "\n")
-
     fun of_subproof ind ctxt proof =
       let
         val ind = ind + 1
@@ -262,13 +256,16 @@
         add_str (of_indent ind ^ "let ")
         #> add_term t1 #> add_str " = " #> add_term t2
         #> add_str "\n"
-      | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) =
+      | add_step ind (Prove (qs, xs, l, t, subproofs, ((ls, ss), (meth :: _) :: _))) =
         add_step_pre ind qs subproofs
         #> (case xs of
              [] => add_str (of_have qs (length subproofs) ^ " ")
            | _ =>
              add_str (of_obtain qs (length subproofs) ^ " ") #> add_frees xs #> add_str " where ")
-        #> add_step_post ind l t facts meth
+        #> add_str (of_label l)
+        #> add_term t
+        #> add_str (" " ^
+             of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^ "\n")
     and add_steps ind = fold (add_step ind)
     and of_proof ind ctxt (Proof (xs, assms, steps)) =
       ("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst