# HG changeset patch
# User wenzelm
# Date 779551528 -7200
# Node ID 760641387b209d84f3a4ca04a927f55326e5884c
# Parent  9cb51c2358ea40fd3bb5025c96f20f05207832dc
replaced lookup_const by Sign.const_type;

diff -r 9cb51c2358ea -r 760641387b20 add_ind_def.ML
--- 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*)
diff -r 9cb51c2358ea -r 760641387b20 datatype.ML
--- 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