replaced add_defns_i by add_defs_i;
changed instant_types: now uses Sign.infer_types;

--- a/Datatype.ML	Fri Aug 19 11:27:19 1994 +0200
+++ b/Datatype.ML	Fri Aug 19 16:18:44 1994 +0200
@@ -103,7 +103,7 @@
                    dtTyp of dt_type list * string |
                    dtRek of dt_type list * string;
 
-local open Syntax.Mixfix
+local open Syntax
            ThyParse
       exception Impossible
 
@@ -214,10 +214,7 @@
 *)
 
 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
 
@@ -505,7 +502,7 @@
                         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