src/HOL/Tools/recdef_package.ML

 fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy =
   let
     val _ = requires_recdef thy;
 
     val name = Sign.intern_const thy raw_name;
-    val bname = NameSpace.base_name name;
+    val bname = Long_Name.base_name name;
     val _ = writeln ("Defining recursive function " ^ quote name ^ " ...");
 
     val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
     val eq_atts = map (map (prep_att thy)) raw_eq_atts;
 

 (** defer_recdef(_i) **)
 
 fun gen_defer_recdef tfl_fn eval_thms raw_name eqs raw_congs thy =
   let
     val name = Sign.intern_const thy raw_name;
-    val bname = NameSpace.base_name name;
+    val bname = Long_Name.base_name name;
 
     val _ = requires_recdef thy;
     val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");
 
     val congs = eval_thms (ProofContext.init thy) raw_congs;