diff -r 9cb51c2358ea -r 760641387b20 datatype.ML
--- 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