author | wenzelm |
Thu, 07 Sep 2000 20:58:54 +0200 | |
changeset 9903 | d087c8dae285 |
parent 9902 | 1ea354905d88 |
child 9904 | 09253f667beb |
--- a/src/Pure/Isar/isar_thy.ML Thu Sep 07 20:57:57 2000 +0200 +++ b/src/Pure/Isar/isar_thy.ML Thu Sep 07 20:58:54 2000 +0200 @@ -446,7 +446,7 @@ val print_result = Pretty.writeln o pretty_result; fun cond_print_result_rule int = - if int then (print_result, Pretty.writeln o pretty_rule) + if int then (print_result, priority o Pretty.string_of o pretty_rule) else (K (), K ()); fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);