--- a/datatype.ML Fri Nov 25 14:21:14 1994 +0100
+++ b/datatype.ML Fri Nov 25 14:39:13 1994 +0100
@@ -13,7 +13,7 @@
local
val mysort = sort;
-open ThyParse;
+open ThyParse HOLogic;
exception Impossible;
exception RecError of string;
@@ -310,8 +310,8 @@
val types = [(tname, datatype_arity, NoSyn)];
val arities =
- let val term_list = replicate datatype_arity ["term"];
- in [(tname, term_list, ["term"])]
+ let val term_list = replicate datatype_arity termS;
+ in [(tname, term_list, termS)]
end;
val datatype_name = pp_typlist1 typevars ^ tname;
@@ -427,7 +427,7 @@
val defpair = mk_defpair (Const(fname,dummyT),rhs)
val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair;
val varT = Type.varifyT T;
- val Some(ftyp) = Sign.const_type sg fname;
+ val ftyp = the (Sign.const_type sg fname);
in
if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT)
then add_defs_i [defpairT] thy