# HG changeset patch
# User wenzelm
# Date 876757679 -7200
# Node ID 73c074f41749081bf4c106a704d7347f67e362b8
# Parent  e694c660055b7174cf8804448f7b6096c9a14199
uses Sign.str_of_sort;

diff -r e694c660055b -r 73c074f41749 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Mon Oct 13 12:51:51 1997 +0200
+++ b/src/Pure/goals.ML	Mon Oct 13 17:47:59 1997 +0200
@@ -155,7 +155,7 @@
                  cat_lines (map (Sign.string_of_term sign) hyps))
 	    else if not (null xshyps) then !result_error_fn state
                 ("Extra sort hypotheses: " ^
-                 commas (map Sorts.str_of_sort xshyps))
+                 commas (map (Sign.str_of_sort sign) xshyps))
 	    else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
 			            (term_of chorn, prop)
 		 then  standard th