author | wenzelm |
Sat, 03 Feb 2001 17:43:34 +0100 | |
changeset 11048 | 2f4976370b7a |
parent 11047 | 10c51288b00d |
child 11049 | 7eef34adb852 |
--- a/src/Pure/Isar/isar_thy.ML Sat Feb 03 17:43:05 2001 +0100 +++ b/src/Pure/Isar/isar_thy.ML Sat Feb 03 17:43:34 2001 +0100 @@ -376,7 +376,7 @@ val print_result = Pretty.writeln o pretty_result; fun cond_print_result_rule int = - if int then (print_result, priority o Pretty.string_of o pretty_rule "Trying") + if int then (print_result, priority o Pretty.string_of o pretty_rule "Attempt") else (K (), K ()); fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);