--- a/src/Pure/theory.ML Mon Nov 06 22:49:16 2000 +0100
+++ b/src/Pure/theory.ML Mon Nov 06 22:50:01 2000 +0100
@@ -324,12 +324,9 @@
datatype overloading = NoOverloading | Useless | Plain;
fun overloading sg declT defT =
- let
- val tsig = Sign.tsig_of sg;
- val T = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT);
- in
- if Type.typ_instance (tsig, declT, T) then NoOverloading
- else if Type.typ_instance (tsig, Type.rem_sorts declT, Type.rem_sorts T) then Useless
+ 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 Plain
end;