# HG changeset patch
# User wenzelm
# Date 809954184 -7200
# Node ID 0901441a7ebf967492a75cc129f8c8a9ac7e2dd5
# Parent  2c0d94151e749c69508ef2d331f9c9716723746b
adapted to new version of shyps-stuff;

diff -r 2c0d94151e74 -r 0901441a7ebf src/Pure/goals.ML
--- a/src/Pure/goals.ML	Fri Sep 01 13:13:19 1995 +0200
+++ b/src/Pure/goals.ML	Fri Sep 01 13:16:24 1995 +0200
@@ -143,7 +143,8 @@
 	    		handle _ => state   (*smash flexflex pairs*)
 	    val ngoals = nprems_of state
             val th = strip_shyps (implies_intr_list cAs state)
-            val {shyps,hyps,prop,sign=sign',...} = rep_thm th
+            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
 		("Signature of proof state has changed!" ^
@@ -153,8 +154,9 @@
             else if not (null hyps) then result_error state
                 ("Additional hypotheses:\n" ^ 
                  cat_lines (map (Sign.string_of_term sign) hyps))
-	    else if not (null shyps) then result_error state
-                ("Pending sort hypotheses: " ^ commas (map Sign.Type.str_of_sort shyps))
+	    else if not (null xshyps) then result_error state
+                ("Extra sort hypotheses: " ^
+                 commas (map Sign.Type.str_of_sort xshyps))
 	    else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
 			            (term_of chorn, prop)
 		 then  standard th