datatype.ML

 		      ^ "   " ^ Sign.string_of_term (sign_of thy) eq);
     in (  name1, ls1
 	, 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 *)
       fun analyse_types (cons, typlist, syn) =
 	let fun analyse(t as dtVar v) =

 	    list_abs_free
 	    (ls @ [(tname,dummyT)]
 	     ,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
 	  if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT)
 	  then add_defs_i [(defname,tdef)] thy