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