--- a/src/Pure/Isar/isar_thy.ML Tue Oct 29 11:32:52 2002 +0100
+++ b/src/Pure/Isar/isar_thy.ML Wed Oct 30 12:18:23 2002 +0100
@@ -326,8 +326,9 @@
val print_result = Pretty.writeln oo pretty_results;
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"))
+fun cond_print_result_rule int = if int
+ then (print_result',
+ priority oo (Pretty.string_of oo pretty_rule "Successful attempt"))
else (K (K ()), K (K ()));
fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);