# HG changeset patch
# User blanchet
# Date 1409237906 -7200
# Node ID 62ec5b1d2f2fee56fa201886f3181acddc1dcbd4
# Parent  27ee844c2b4dff4f4a35f073128a2945189995de
three-line 'obtain' format for generated Isar proofs

diff -r 27ee844c2b4d -r 62ec5b1d2f2f src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Aug 28 15:51:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Aug 28 16:58:26 2014 +0200
@@ -337,7 +337,10 @@
         add_step_pre ind qs subs
         #> (case xs of
             [] => add_str (of_have qs (length subs) ^ " ")
-          | _ => add_str (of_obtain qs (length subs) ^ " ") #> add_frees xs #> add_str " where ")
+          | _ =>
+            add_str (of_obtain qs (length subs) ^ " ")
+            #> add_frees xs
+            #> add_str (" where\n" ^ of_indent (ind + 1)))
         #> add_str (of_label l)
         #> add_term t
         #> add_str ("\n" ^ of_indent (ind + 1) ^ of_method ls ss meth ^