# HG changeset patch
# User paulson
# Date 909161305 -7200
# Node ID 5a571d57183f0535872af0a629e707886bdb640a
# Parent  387b5bf9326a3a904e475912cf7c2edf8e453131
better reporting of "Additional hypotheses" in a locale

diff -r 387b5bf9326a -r 5a571d57183f src/Pure/goals.ML
--- 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))