--- a/src/Pure/goals.ML Fri Oct 23 18:47:44 1998 +0200
+++ b/src/Pure/goals.ML Fri Oct 23 18:48:25 1998 +0200
@@ -181,8 +181,11 @@
(string_of_int ngoals ^ " unsolved goals!")
else if (not (null hyps) andalso (not (Locale.in_locale hyps sign)))
then !result_error_fn state
- ("Additional hypotheses:\n" ^
- cat_lines (map (Sign.string_of_term sign) hyps))
+ ("Additional hypotheses:\n" ^
+ cat_lines
+ (map (Sign.string_of_term sign)
+ (filter (fn x => (not (Locale.in_locale [x] sign)))
+ hyps)))
else if not (null xshyps) then !result_error_fn state
("Extra sort hypotheses: " ^
commas (map (Sign.str_of_sort sign) xshyps))