# HG changeset patch # User wenzelm # Date 877337605 -7200 # Node ID 83f908ed3c04aa04e6c4b58e3abc79eb5a28055b # Parent c20fbe3cb94f887cb4022384b81c202047c6f740 Sign.base_name; diff -r c20fbe3cb94f -r 83f908ed3c04 src/ZF/add_ind_def.ML --- a/src/ZF/add_ind_def.ML Mon Oct 20 10:52:32 1997 +0200 +++ b/src/ZF/add_ind_def.ML Mon Oct 20 10:53:25 1997 +0200 @@ -87,7 +87,7 @@ val rec_names = map (#1 o dest_Const) rec_hds and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); - val rec_base_names = map NameSpace.base rec_names; + val rec_base_names = map Sign.base_name rec_names; val dummy = assert_all Syntax.is_identifier rec_base_names (fn a => "Base name of recursive set not an identifier: " ^ a); diff -r c20fbe3cb94f -r 83f908ed3c04 src/ZF/indrule.ML --- a/src/ZF/indrule.ML Mon Oct 20 10:52:32 1997 +0200 +++ b/src/ZF/indrule.ML Mon Oct 20 10:53:25 1997 +0200 @@ -26,7 +26,7 @@ val (Const(_,recT),rec_params) = strip_comb (hd Inductive.rec_tms); val big_rec_name = - Sign.intern_const sign (space_implode "_" (map NameSpace.base Intr_elim.rec_names)); + Sign.intern_const sign (space_implode "_" (map Sign.base_name Intr_elim.rec_names)); val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); @@ -119,7 +119,7 @@ mutual recursion to invariably be a disjoint sum.*) fun mk_predpair rec_tm = let val rec_name = (#1 o dest_Const o head_of) rec_tm - val pfree = Free(pred_name ^ "_" ^ NameSpace.base rec_name, + val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name, elem_factors ---> Ind_Syntax.oT) val qconcl = foldr Ind_Syntax.mk_all diff -r c20fbe3cb94f -r 83f908ed3c04 src/ZF/intr_elim.ML --- 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 ^