# HG changeset patch
# User wenzelm
# Date 807290465 -7200
# Node ID b1a04399f530bf4f248b681cf7178803eeafd563
# Parent  59ed8ef1a3a17d580fc26a76b9228f68dc23d41b
modified prepare_proof to handle shyps;

diff -r 59ed8ef1a3a1 -r b1a04399f530 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Tue Aug 01 17:20:42 1995 +0200
+++ b/src/Pure/goals.ML	Tue Aug 01 17:21:05 1995 +0200
@@ -142,8 +142,8 @@
         let val state = Sequence.hd (flexflex_rule state)
 	    		handle _ => state   (*smash flexflex pairs*)
 	    val ngoals = nprems_of state
-            val th = implies_intr_list cAs state
-            val {hyps,prop,sign=sign',...} = rep_thm th
+            val th = strip_shyps (implies_intr_list cAs state)
+            val {shyps,hyps,prop,sign=sign',...} = rep_thm 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,6 +153,8 @@
             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 Pattern.matches (#tsig(Sign.rep_sg sign)) 
 			            (term_of chorn, prop)
 		 then  standard th