author | wenzelm |
Fri, 09 May 2014 22:14:06 +0200 | |
changeset 56933 | b47193851dc6 |
parent 56932 | 11a4001b06c6 |
child 56934 | 2c664c817bdf |
--- 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