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 40132 7ee65dbffa31
parent 39616 8052101883c3
child 40642 99c6ce92669b 
--- a/src/Pure/Isar/proof.ML	Mon Oct 25 20:24:13 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Oct 25 21:06:56 2010 +0200
@@ -972,7 +972,7 @@
       if ! testing then () else Proof_Display.print_results int ctxt res;
     fun print_rule ctxt th =
       if ! testing then rule := SOME th
-      else if int then priority (Proof_Display.string_of_rule ctxt "Successful" th)
+      else if int then Output.urgent_message (Proof_Display.string_of_rule ctxt "Successful" th)
       else ();
     val test_proof =
       try (local_skip_proof true)
isabelle