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