src/Pure/goals.ML
changeset 10745 0f3537fad0f3
parent 10487 97d25c125c61
child 11554 685daff01da4
equal deleted inserted replaced
10744:5d142ca01b8e 10745:0f3537fad0f3
   131 (*Default action is to print an error message; could be suppressed for
   131 (*Default action is to print an error message; could be suppressed for
   132   special applications.*)
   132   special applications.*)
   133 fun result_error_default state msg : thm =
   133 fun result_error_default state msg : thm =
   134  (writeln "Bad final proof state:";
   134  (writeln "Bad final proof state:";
   135   print_goals (!goals_limit) state;
   135   print_goals (!goals_limit) state;
   136   writeln msg; raise ERROR);
   136   writeln msg; error "Proof failed");
   137 
   137 
   138 val result_error_fn = ref result_error_default;
   138 val result_error_fn = ref result_error_default;
   139 
   139 
   140 (* alternative to standard: this function does not discharge the hypotheses
   140 (* alternative to standard: this function does not discharge the hypotheses
   141    first. Is used for locales, in the following function prepare_proof *)
   141    first. Is used for locales, in the following function prepare_proof *)