replaced lookup_const by Sign.const_type;
authorwenzelm
Wed, 14 Sep 1994 16:05:39 +0200
changeset 612 1ebe4d36dedc
parent 611 11098f505bfe
child 613 f9eb0f819642
replaced lookup_const by Sign.const_type;
src/ZF/add_ind_def.ML
--- a/src/ZF/add_ind_def.ML	Wed Sep 14 16:02:06 1994 +0200
+++ b/src/ZF/add_ind_def.ML	Wed Sep 14 16:05:39 1994 +0200
@@ -94,7 +94,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*)