# HG changeset patch
# User wenzelm
# Date 968353134 -7200
# Node ID d087c8dae285a43e595625ec1a30381af736c8a9
# Parent  1ea354905d888a2e60489c08fd9e7acdab35a578
print rule: priority;

diff -r 1ea354905d88 -r d087c8dae285 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Sep 07 20:57:57 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Sep 07 20:58:54 2000 +0200
@@ -446,7 +446,7 @@
 val print_result = Pretty.writeln o pretty_result;
 
 fun cond_print_result_rule int =
-  if int then (print_result, Pretty.writeln o pretty_rule)
+  if int then (print_result, priority o Pretty.string_of o pretty_rule)
   else (K (), K ());
 
 fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);