src/HOL/Tools/old_primrec_package.ML

   let
     val rhs = fold_rev (fn T => fn t => Abs ("", T, t))
                     ((map snd ls) @ [dummyT])
                     (list_comb (Const (rec_name, dummyT),
                                 fs @ map Bound (0 ::(length ls downto 1))))
-    val def_name = NameSpace.base_name fname ^ "_" ^ NameSpace.base_name tname ^ "_def";
+    val def_name = Long_Name.base_name fname ^ "_" ^ Long_Name.base_name tname ^ "_def";
     val def_prop =
       singleton (Syntax.check_terms (ProofContext.init thy))
         (Logic.mk_equals (Const (fname, dummyT), rhs));
   in (def_name, def_prop) end;
 

     val nameTs2 = map fst rec_eqns;
     val _ = if gen_eq_set (op =) (nameTs1, nameTs2) then ()
             else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
               "\nare not mutually recursive");
     val primrec_name =
-      if alt_name = "" then (space_implode "_" (map (NameSpace.base_name o #1) defs)) else alt_name;
+      if alt_name = "" then (space_implode "_" (map (Long_Name.base_name o #1) defs)) else alt_name;
     val (defs_thms', thy') =
       thy
       |> Sign.add_path primrec_name
       |> fold_map def (map (fn (name, t) => ((name, []), t)) defs');
     val rewrites = (map mk_meta_eq rec_rewrites) @ map snd defs_thms';