src/Pure/goals.ML

   val push_proof	: unit -> unit
   val read		: string -> term
   val ren		: string -> int -> unit
   val restore_proof	: proof -> thm list
   val result		: unit -> thm  
+  val result_error_ref  : (thm -> string -> thm) ref
   val rotate_proof	: unit -> thm list
   val uresult		: unit -> thm  
   val save_proof	: unit -> proof
   val topthm		: unit -> thm
   val undo		: unit -> unit

   in  case stamps of
         [stamp] => "\nNew theory: " ^ !stamp
       | _       => "\nNew theories: " ^ space_implode ", " (map ! stamps)
   end;
 
+(*Default action is to print an error message; could be suppressed for
+  special applications.*)
+fun result_error_default state msg : thm = 
+  (writeln ("Bad final proof state:");
+   !print_goals_ref (!goals_limit) state;
+   error msg);
+
+val result_error_ref = ref result_error_default;
+
 (*Common treatment of "goal" and "prove_goal":
   Return assumptions, initial proof state, and function to make result. *)
 fun prepare_proof rths chorn =
   let val {sign, t=horn,...} = rep_cterm chorn;
       val (_,As,B) = Logic.strip_horn(horn);
       val cAs = map (cterm_of sign) As;
       val prems = map (rewrite_rule rths o forall_elim_vars(0) o assume) cAs
       and st0 = (rewrite_goals_rule rths o trivial) (cterm_of sign B)
-      fun result_error state msg = 
-        (writeln ("Bad final proof state:");
- 	 !print_goals_ref (!goals_limit) state;
-	 error msg)
       (*discharges assumptions from state in the order they appear in goal;
 	checks (if requested) that resulting theorem is equivalent to goal. *)
       fun mkresult (check,state) =
         let val state = Sequence.hd (flexflex_rule state)
 	    		handle THM _ => state   (*smash flexflex pairs*)
 	    val ngoals = nprems_of state
             val th = strip_shyps (implies_intr_list cAs state)
             val {hyps,prop,sign=sign',...} = rep_thm th
             val xshyps = extra_shyps th;
         in  if not check then standard th
-	    else if not (Sign.eq_sg(sign,sign')) then result_error state
+	    else if not (Sign.eq_sg(sign,sign')) then !result_error_ref state
 		("Signature of proof state has changed!" ^
 		 sign_error (sign,sign'))
-            else if ngoals>0 then result_error state
+            else if ngoals>0 then !result_error_ref state
 		(string_of_int ngoals ^ " unsolved goals!")
-            else if not (null hyps) then result_error state
+            else if not (null hyps) then !result_error_ref state
                 ("Additional hypotheses:\n" ^ 
                  cat_lines (map (Sign.string_of_term sign) hyps))
-	    else if not (null xshyps) then result_error state
+	    else if not (null xshyps) then !result_error_ref state
                 ("Extra sort hypotheses: " ^
                  commas (map Type.str_of_sort xshyps))
 	    else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
 			            (term_of chorn, prop)
 		 then  standard th 
-	    else  result_error state "proved a different theorem"
+	    else  !result_error_ref state "proved a different theorem"
         end
   in
      if Sign.eq_sg(sign, #sign(rep_thm st0))
      then (prems, st0, mkresult)
      else error ("Definitions would change the proof state's signature" ^