diff -r 8325414a370a -r 6be2f3e03786 datatype.ML
--- 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