Datatype.ML

 (*used for constructor parameters*)
 datatype dt_type = dtVar of string |
                    dtTyp of dt_type list * string |
                    dtRek of dt_type list * string;
 
-local open Syntax.Mixfix
+local open Syntax
            ThyParse
       exception Impossible
 
 val is_Rek = (fn dtRek _ => true  |  _  => false);
 

 (* take datatype and eqns and return a properly type-instantiated 
    application of the prim-rec-combinator which solves eqns.
 *)
 
 fun instant_types thy t =
-let val rs = Sign.rep_sg(sign_of thy);  
-in  fst(Type.infer_types( #tsig rs,#const_tab rs, K None, K None
-		        , TVar(("",0),[]), t))
-end;
+  fst (Sign.infer_types (sign_of thy) (K None) (K None) (t, TVar(("",0),[])));
 
 in
 
 fun add_datatype (typevars, tname, cons_list') thy = 
   let (*search for free type variables and convert recursive *)

           val (fname,rfuns) = funs_from_eqns cons_list teqns
           val rhs = Abs(tname, dummyT,
                         list_comb(rec_comb, Bound 0 :: rev rfuns))
           val def = Const("==",dummyT) $ Const(fname,dummyT) $ rhs
           val tdef = instant_types thy def
-      in add_defns_i [(fname ^ "_def", tdef)] thy end;
+      in add_defs_i [(fname ^ "_def", tdef)] thy end;
 
   in (thy
      |> add_types types
      |> add_arities arities
      |> add_consts consts