--- a/add_ind_def.ML Sun Sep 11 10:31:17 1994 +0200
+++ b/add_ind_def.ML Wed Sep 14 16:05:28 1994 +0200
@@ -65,7 +65,7 @@
val _ = assert_all Syntax.is_identifier rec_names
(fn a => "Name of recursive set not an identifier: " ^ a);
- val _ = assert_all (is_some o lookup_const sign) rec_names
+ val _ = assert_all (is_some o Sign.const_type sign) rec_names
(fn a => "Recursive set not previously declared as constant: " ^ a);
local (*Checking the introduction rules*)
--- a/datatype.ML Sun Sep 11 10:31:17 1994 +0200
+++ b/datatype.ML Wed Sep 14 16:05:28 1994 +0200
@@ -239,7 +239,7 @@
fun instantiate_types thy t =
let val sg = sign_of thy
val rsg = Sign.rep_sg sg
- in fst(Type.infer_types(#tsig rsg, lookup_const sg, K None, K None,
+ in fst(Type.infer_types(#tsig rsg, Sign.const_type sg, K None, K None,
TVar(("",0),[]), t))
end;
@@ -535,7 +535,7 @@
val (defname,def) = mk_defpair (Const(fname,dummyT),rhs)
val tdef as ( _ $ Const(_,T) $ _ ) = instantiate_types thy def;
val varT = Type.varifyT T;
- val Some(ftyp) = lookup_const sg fname;
+ val Some(ftyp) = Sign.const_type sg fname;
in
if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT)
then add_defs_i [(defname,tdef)] thy