# HG changeset patch
# User paulson
# Date 840537617 -7200
# Node ID 3d1d73e3d185d53459f11c8501dae51ec2d1e529
# Parent  6f97cb16e453bae28451ce3e0a705638e9ae8844
Added ref to allow suppression of error msgs

diff -r 6f97cb16e453 -r 3d1d73e3d185 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Tue Aug 20 12:39:30 1996 +0200
+++ b/src/Pure/goals.ML	Tue Aug 20 12:40:17 1996 +0200
@@ -61,6 +61,7 @@
   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
@@ -115,6 +116,15 @@
       | _       => "\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 =
@@ -123,10 +133,6 @@
       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) =
@@ -137,21 +143,21 @@
             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))