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