--- a/datatype.ML Sun Sep 11 10:31:17 1994 +0200
+++ b/datatype.ML Wed Sep 14 16:05:28 1994 +0200
@@ -239,7 +239,7 @@
fun instantiate_types thy t =
let val sg = sign_of thy
val rsg = Sign.rep_sg sg
- in fst(Type.infer_types(#tsig rsg, lookup_const sg, K None, K None,
+ in fst(Type.infer_types(#tsig rsg, Sign.const_type sg, K None, K None,
TVar(("",0),[]), t))
end;
@@ -535,7 +535,7 @@
val (defname,def) = mk_defpair (Const(fname,dummyT),rhs)
val tdef as ( _ $ Const(_,T) $ _ ) = instantiate_types thy def;
val varT = Type.varifyT T;
- val Some(ftyp) = lookup_const sg fname;
+ val Some(ftyp) = Sign.const_type sg fname;
in
if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT)
then add_defs_i [(defname,tdef)] thy