--- 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