author | wenzelm |
Wed, 14 Sep 1994 16:05:39 +0200 | |
changeset 612 | 1ebe4d36dedc |
parent 611 | 11098f505bfe |
child 613 | f9eb0f819642 |
--- 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*)