# HG changeset patch # User nipkow # Date 1035976703 -3600 # Node ID bc63c3b2b3e78faa9138218942d83df5916f31fd # Parent 0b8fbcf65d736990c351a15e6451f284e9242414 modified msg diff -r 0b8fbcf65d73 -r bc63c3b2b3e7 src/Pure/Isar/isar_thy.ML --- 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);