# HG changeset patch
# User paulson
# Date 965900020 -7200
# Node ID 5cadc8146573de67e61505ef9f022c095cebd89f
# Parent  bfee45ac5d3886771685dd5375e5bf31f9cddc4d
the "nocheck" versions of goal functions now standardize their result

diff -r bfee45ac5d38 -r 5cadc8146573 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Aug 10 11:30:39 2000 +0200
+++ b/src/Pure/goals.ML	Thu Aug 10 11:33:40 2000 +0200
@@ -212,7 +212,8 @@
             val ath = implies_intr_list cAs state
             val th = ath RS Drule.rev_triv_goal
             val {hyps,prop,sign=sign',...} = rep_thm th
-        in  if not check then th
+            val final_th = if (null(hyps)) then standard th else varify th
+        in  if not check then final_th
 	    else if not (Sign.eq_sg(sign,sign')) then !result_error_fn state
 		("Signature of proof state has changed!" ^
 		 sign_error (sign,sign'))
@@ -227,8 +228,7 @@
 		      hyps)))
 	    else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
 			            (term_of chorn, prop)
-		 then  (if (null(hyps)) then standard th 
-                       else varify th)
+		 then final_th
 	    else  !result_error_fn state "proved a different theorem"
         end
   in