# 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 ^