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*)