--- 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 ^