# HG changeset patch
# User wenzelm
# Date 1119457588 -7200
# Node ID d4de40568ab193af576029e1391b3b674d74a311
# Parent  25a7459d4d4adfa13980c9fdd76e7fa397e6a3e1
tuned;

diff -r 25a7459d4d4a -r d4de40568ab1 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Jun 22 11:20:45 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Wed Jun 22 18:26:28 2005 +0200
@@ -327,10 +327,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 "Successful attempt"))
-  else (K (K ()), K (K ()));
+fun cond_print_result_rule true =
+      (print_result', priority oo (Pretty.string_of oo pretty_rule "Successful attempt"))
+  | cond_print_result_rule false = (K (K ()), K (K ()));
 
 fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);