diff -r a9f7ff3a464c -r 85f62d491ff7 datatype.ML
--- a/datatype.ML	Wed Sep 21 15:40:41 1994 +0200
+++ b/datatype.ML	Mon Sep 26 18:04:43 1994 +0100
@@ -234,14 +234,6 @@
 	, check_and_sort (length cs, trans_recs' [] (eq1::eqs)))
     end ;
 
-
-fun instantiate_types thy t =
-  let val sg = sign_of thy
-      val rsg = Sign.rep_sg sg
-  in  fst(Type.infer_types(#tsig rsg, Sign.const_type sg, K None, K None,
-			   TVar(("",0),[]), t))
-  end;
-
 in
   fun add_datatype (typevars, tname, cons_list') thy = 
     let (*search for free type variables and convert recursive *)
@@ -530,8 +522,8 @@
 	     ,list_comb(rec_comb
 			, fns @ map Bound (0 ::(length ls downto 1))));
           val sg = sign_of thy;
-          val (defname,def) =  mk_defpair (Const(fname,dummyT),rhs)
-	  val tdef as ( _ $ Const(_,T) $ _ ) = instantiate_types thy def;
+          val defpair as (defname,_) =  mk_defpair (Const(fname,dummyT),rhs)
+	  val (_,tdef as ( _ $ Const(_,T) $ _ )) = inferT_axm sg defpair;
 	  val varT = Type.varifyT T;
           val Some(ftyp) = Sign.const_type sg fname;
 	in