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