# HG changeset patch
# User wenzelm
# Date 1085167557 -7200
# Node ID 214926b0970cf0045ad8b3cd36014310ca799a65
# Parent  9776f0c747c865a66d4ae7820fc1a1514d53c3bf
Type.strip_sorts;

diff -r 9776f0c747c8 -r 214926b0970c src/Pure/theory.ML
--- 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;