Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/proof.ML
changeset 56933 b47193851dc6
parent 56932 11a4001b06c6
child 57486 2131b6633529 
--- a/src/Pure/Isar/proof.ML	Fri May 09 22:04:50 2014 +0200
+++ b/src/Pure/Isar/proof.ML	Fri May 09 22:14:06 2014 +0200
@@ -1064,7 +1064,10 @@
     fun print_rule ctxt th =
       if ! testing then rule := SOME th
       else if int then
-        writeln (Markup.markup Markup.state (Proof_Display.string_of_rule ctxt "Successful" th))
+        Proof_Display.string_of_rule ctxt "Successful" th
+        |> Markup.markup Markup.text_fold
+        |> Markup.markup Markup.state
+        |> writeln
       else ();
     val test_proof =
       local_skip_proof true
isabelle