Type.strip_sorts;

--- a/src/Pure/theory.ML	Fri May 21 21:25:34 2004 +0200
+++ b/src/Pure/theory.ML	Fri May 21 21:25:57 2004 +0200
@@ -344,7 +344,7 @@
 fun overloading sg declT defT =
   let val T = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT) in
     if Sign.typ_instance sg (declT, T) then NoOverloading
-    else if Sign.typ_instance sg (Type.rem_sorts declT, Type.rem_sorts T) then Useless
+    else if Sign.typ_instance sg (Type.strip_sorts declT, Type.strip_sorts T) then Useless
     else Plain
   end;