src/Pure/goals.ML
changeset 5748 5a571d57183f
parent 5729 5d66410cceae
child 5775 cbd439ed350d
--- 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))