src/ZF/Tools/primrec_package.ML

     val recursor = head_of (#1 (hd recursor_pairs))
 
     (** make definition **)
 
     (*the recursive argument*)
-    val rec_arg = Free (Name.variant (map #1 (ls@rs)) (NameSpace.base_name big_rec_name),
+    val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Long_Name.base_name big_rec_name),
                         Ind_Syntax.iT)
 
     val def_tm = Logic.mk_equals
                     (subst_bound (rec_arg, fabs),
                      list_comb (recursor,

   in
       if !Ind_Syntax.trace then
             writeln ("primrec def:\n" ^
                      Syntax.string_of_term_global thy def_tm)
       else();
-      (NameSpace.base_name fname ^ "_" ^ NameSpace.base_name big_rec_name ^ "_def",
+      (Long_Name.base_name fname ^ "_" ^ Long_Name.base_name big_rec_name ^ "_def",
        def_tm)
   end;
 
 
 (* prepare functions needed for definitions *)

     val SOME (fname, ftype, ls, rs, con_info, eqns) =
       List.foldr (process_eqn thy) NONE eqn_terms;
     val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
 
     val ([def_thm], thy1) = thy
-      |> Sign.add_path (NameSpace.base_name fname)
+      |> Sign.add_path (Long_Name.base_name fname)
       |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)];
 
     val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
     val eqn_thms =
       eqn_terms |> map (fn t =>