--- 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