tuned;
authorwenzelm
Wed Jun 22 18:26:28 2005 +0200 (2005-06-22)
changeset 16529d4de40568ab1
parent 16528 25a7459d4d4a
child 16530 3e493fa130a3
tuned;
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Jun 22 11:20:45 2005 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Jun 22 18:26:28 2005 +0200
     1.3 @@ -327,10 +327,9 @@
     1.4  val print_result = Pretty.writeln oo pretty_results;
     1.5  fun print_result' ctxt (k, res) = print_result ctxt ((k, ""), res);
     1.6  
     1.7 -fun cond_print_result_rule int = if int
     1.8 -  then (print_result',
     1.9 -        priority oo (Pretty.string_of oo pretty_rule "Successful attempt"))
    1.10 -  else (K (K ()), K (K ()));
    1.11 +fun cond_print_result_rule true =
    1.12 +      (print_result', priority oo (Pretty.string_of oo pretty_rule "Successful attempt"))
    1.13 +  | cond_print_result_rule false = (K (K ()), K (K ()));
    1.14  
    1.15  fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);
    1.16