# HG changeset patch
# User wenzelm
# Date 779551539 -7200
# Node ID 1ebe4d36dedc2526d014e75a5eac820230d2ed66
# Parent  11098f505bfeb8afec03bf0d292093fb51e44f62
replaced lookup_const by Sign.const_type;

diff -r 11098f505bfe -r 1ebe4d36dedc 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*)