src/Pure/Isar/isar_thy.ML
changeset 11048 2f4976370b7a
parent 10935 808e9dbc68c4
child 11717 d808005e6e08
equal deleted inserted replaced
11047:10c51288b00d 11048:2f4976370b7a
   374 in
   374 in
   375 
   375 
   376 val print_result = Pretty.writeln o pretty_result;
   376 val print_result = Pretty.writeln o pretty_result;
   377 
   377 
   378 fun cond_print_result_rule int =
   378 fun cond_print_result_rule int =
   379   if int then (print_result, priority o Pretty.string_of o pretty_rule "Trying")
   379   if int then (print_result, priority o Pretty.string_of o pretty_rule "Attempt")
   380   else (K (), K ());
   380   else (K (), K ());
   381 
   381 
   382 fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);
   382 fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);
   383 
   383 
   384 fun check_goal false state = state
   384 fun check_goal false state = state