# HG changeset patch
# User wenzelm
# Date 1011908620 -3600
# Node ID ac191fb20ff1d1bbacdf544dc15ded80f372dd40
# Parent  afa356dbcb15e12d643fdac0f2706655845d2c9f
cond_print_result_rule: priority (again) instead of slightly
  ill-behaved tracing output;

diff -r afa356dbcb15 -r ac191fb20ff1 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Jan 24 22:42:14 2002 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Thu Jan 24 22:43:40 2002 +0100
@@ -439,7 +439,7 @@
 fun print_result' ctxt (k, res) = print_result ctxt ((k, ""), res);
 
 fun cond_print_result_rule int =
-  if int then (print_result', tracing oo (Pretty.string_of oo pretty_rule "Attempt"))
+  if int then (print_result', priority oo (Pretty.string_of oo pretty_rule "Attempt"))
   else (K (K ()), K (K ()));
 
 fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);