1.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Dec 27 16:45:19 2001 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Dec 27 16:46:04 2001 +0100
     1.3 @@ -406,7 +406,7 @@
     1.4  fun print_result' ctxt (k, res) = print_result ctxt ((k, ""), res);
     1.5  
     1.6  fun cond_print_result_rule int =
     1.7 -  if int then (print_result', priority oo (Pretty.string_of oo pretty_rule "Attempt"))
     1.8 +  if int then (print_result', tracing oo (Pretty.string_of oo pretty_rule "Attempt"))
     1.9    else (K (K ()), K (K ()));
    1.10  
    1.11  fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);