src/ZF/intr_elim.ML

      and Fp: FP and Pr : PR and Su : SU) 
     : sig include INTR_ELIM INTR_ELIM_AUX end =
 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 ^ 
               " would clash with the theory of the same name!");