changeset 612 | 1ebe4d36dedc |
parent 591 | 5a6b0ed377cb |
child 727 | 711e4eb8c213 |
--- 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*)