# HG changeset patch
# User wenzelm
# Date 1009467964 -3600
# Node ID f0cf30cd7e4c171b5bb47fa731cb3ed11b6dccd0
# Parent  30ec65eaaf5f1d14c3e5cff3822f3d0289d355b1
solve rule: tracing instead of priority;

diff -r 30ec65eaaf5f -r f0cf30cd7e4c src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Dec 27 16:45:19 2001 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Thu Dec 27 16:46:04 2001 +0100
@@ -406,7 +406,7 @@
 fun print_result' ctxt (k, res) = print_result ctxt ((k, ""), res);
 
 fun cond_print_result_rule int =
-  if int then (print_result', priority oo (Pretty.string_of oo pretty_rule "Attempt"))
+  if int then (print_result', tracing oo (Pretty.string_of oo pretty_rule "Attempt"))
   else (K (K ()), K (K ()));
 
 fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);