changeset 3939 | 83f908ed3c04 |
parent 3925 | 90f499226ab9 |
child 3978 | 7e1cfed19d94 |
--- a/src/ZF/intr_elim.ML Mon Oct 20 10:52:32 1997 +0200 +++ b/src/ZF/intr_elim.ML Mon Oct 20 10:53:25 1997 +0200 @@ -48,7 +48,7 @@ let val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms; -val big_rec_base_name = space_implode "_" (map NameSpace.base rec_names); +val big_rec_base_name = space_implode "_" (map Sign.base_name rec_names); val _ = deny (big_rec_base_name mem map ! (stamps_of_thy Inductive.thy)) ("Definition " ^ big_rec_base_name ^