# HG changeset patch
# User wenzelm
# Date 760280120 -3600
# Node ID d7130a753ecf16868a269b0bdfd46983828970d4
# Parent  7532f95d7f447ea3d7b5f3006454c240dfd4ae1b
replaced eq_sg by Sign.eq_sg;

diff -r 7532f95d7f44 -r d7130a753ecf src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Feb 03 13:55:03 1994 +0100
+++ b/src/Pure/goals.ML	Thu Feb 03 13:55:20 1994 +0100
@@ -142,7 +142,7 @@
             val th = implies_intr_list cAs state
             val {hyps,prop,sign=sign',...} = rep_thm th
         in  if not check then standard th
-	    else if not (eq_sg(sign,sign')) then result_error state
+	    else if not (Sign.eq_sg(sign,sign')) then result_error state
 		("Signature of proof state has changed!" ^
 		 sign_error (sign,sign'))
             else if ngoals>0 then result_error state
@@ -156,7 +156,7 @@
 	    else  result_error state "proved a different theorem"
         end
   in  
-     if eq_sg(sign, #sign(rep_thm st0)) 
+     if Sign.eq_sg(sign, #sign(rep_thm st0)) 
      then (prems, st0, mkresult)
      else error ("Definitions would change the proof state's signature" ^
 		 sign_error (sign, #sign(rep_thm st0)))