# HG changeset patch
# User blanchet
# Date 1391190196 -3600
# Node ID 77953325d5f1ff07a359471fbddc6abe524ab01e
# Parent  b6c926e67350d7f48a833d53eb6dcb379c28216d
more concise Isar output

diff -r b6c926e67350 -r 77953325d5f1 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 16:58:58 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
@@ -160,7 +160,7 @@
 
     val register_fixes = map Free #> fold Variable.auto_fixes
 
-    fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
+    fun add_str s' = apfst (suffix s')
 
     fun of_indent ind = replicate_string (ind * indent_size) " "
     fun of_moreover ind = of_indent ind ^ "moreover\n"
@@ -215,14 +215,6 @@
       | of_method ls ss Meson_Method = using_facts ls [] ^ by_facts "meson" [] ss
       | of_method ls ss meth = using_facts ls ss ^ by_method meth
 
-    fun of_byline ind (ls, ss) meth =
-      let
-        val ls = ls |> sort_distinct label_ord
-        val ss = ss |> sort_distinct string_ord
-      in
-        "\n" ^ of_indent (ind + 1) ^ of_method ls ss meth
-      end
-
     fun of_free (s, T) =
       maybe_quote s ^ " :: " ^
       maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
@@ -232,21 +224,22 @@
 
     fun add_fix _ [] = I
       | add_fix ind xs =
-        add_suffix (of_indent ind ^ "fix ")
+        add_str (of_indent ind ^ "fix ")
         #> add_frees xs
-        #> add_suffix "\n"
+        #> add_str "\n"
 
     fun add_assm ind (l, t) =
-      add_suffix (of_indent ind ^ "assume " ^ of_label l)
+      add_str (of_indent ind ^ "assume " ^ of_label l)
       #> add_term t
-      #> add_suffix "\n"
+      #> add_str "\n"
 
     fun add_assms ind assms = fold (add_assm ind) assms
 
-    fun add_step_post ind l t facts meth =
-      add_suffix (of_label l)
+    fun add_step_post ind l t (ls, ss) meth =
+      add_str (of_label l)
       #> add_term t
-      #> add_suffix (of_byline ind facts meth ^ "\n")
+      #> add_str (" " ^
+           of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^ "\n")
 
     fun of_subproof ind ctxt proof =
       let
@@ -266,19 +259,15 @@
     and add_step_pre ind qs subproofs (s, ctxt) =
       (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
     and add_step ind (Let (t1, t2)) =
-        add_suffix (of_indent ind ^ "let ")
-        #> add_term t1
-        #> add_suffix " = "
-        #> add_term t2
-        #> add_suffix "\n"
+        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_pre ind qs subproofs
         #> (case xs of
-            [] => add_suffix (of_have qs (length subproofs) ^ " ")
-          | _ =>
-            add_suffix (of_obtain qs (length subproofs) ^ " ")
-            #> add_frees xs
-            #> add_suffix " where ")
+             [] => 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
     and add_steps ind = fold (add_step ind)
     and of_proof ind ctxt (Proof (xs, assms, steps)) =