Type.strip_sorts;
authorwenzelm
Fri May 21 21:25:57 2004 +0200 (2004-05-21)
changeset 14789214926b0970c
parent 14788 9776f0c747c8
child 14790 0d984ee030a1
Type.strip_sorts;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Fri May 21 21:25:34 2004 +0200
     1.2 +++ b/src/Pure/theory.ML	Fri May 21 21:25:57 2004 +0200
     1.3 @@ -344,7 +344,7 @@
     1.4  fun overloading sg declT defT =
     1.5    let val T = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT) in
     1.6      if Sign.typ_instance sg (declT, T) then NoOverloading
     1.7 -    else if Sign.typ_instance sg (Type.rem_sorts declT, Type.rem_sorts T) then Useless
     1.8 +    else if Sign.typ_instance sg (Type.strip_sorts declT, Type.strip_sorts T) then Useless
     1.9      else Plain
    1.10    end;
    1.11