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,