# HG changeset patch
# User wenzelm
# Date 861207730 -7200
# Node ID 97ae96c72d8c07be76e62b9cb5e5173dde221978
# Parent  842be30dc3362db8ef76890d32204a1a929505ef
Sorts.str_of_sort;

diff -r 842be30dc336 -r 97ae96c72d8c src/Pure/goals.ML
--- a/src/Pure/goals.ML	Wed Apr 16 18:21:00 1997 +0200
+++ b/src/Pure/goals.ML	Wed Apr 16 18:22:10 1997 +0200
@@ -154,7 +154,7 @@
                  cat_lines (map (Sign.string_of_term sign) hyps))
 	    else if not (null xshyps) then !result_error_ref state
                 ("Extra sort hypotheses: " ^
-                 commas (map Type.str_of_sort xshyps))
+                 commas (map Sorts.str_of_sort xshyps))
 	    else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
 			            (term_of chorn, prop)
 		 then  standard th 
diff -r 842be30dc336 -r 97ae96c72d8c src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Apr 16 18:21:00 1997 +0200
+++ b/src/Pure/thm.ML	Wed Apr 16 18:22:10 1997 +0200
@@ -502,7 +502,7 @@
              not (!force_strip_shyps) then shyps'
           else    (* FIXME tmp *)
               (warning ("Removed sort hypotheses: " ^
-                        commas (map Type.str_of_sort (shyps' \\ sorts)));
+                        commas (map Sorts.str_of_sort (shyps' \\ sorts)));
                warning "Let's hope these sorts are non-empty!";
            sorts)),
       hyps = hyps,