# HG changeset patch
# User blanchet
# Date 1409179237 -7200
# Node ID 1d9edd48647942a6fc3d3bb07d66d0976014bb9a
# Parent  decb3e2528e7a1b80827505b4ad774bb6be773c5
reintroduced two-line-per-inference Isar proof format

diff -r decb3e2528e7 -r 1d9edd486479 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Aug 28 00:40:19 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Aug 28 00:40:37 2014 +0200
@@ -340,7 +340,7 @@
           | _ => add_str (of_obtain qs (length subs) ^ " ") #> add_frees xs #> add_str " where ")
         #> add_str (of_label l)
         #> add_term t
-        #> add_str (" " ^ of_method ls ss meth ^
+        #> add_str ("\n" ^ of_indent (ind + 1) ^ of_method ls ss meth ^
           (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
     and add_steps ind = fold (add_step ind)
     and of_proof ind ctxt (Proof (xs, assms, steps)) =