src/HOL/Tools/recdef_package.ML

 val hints =
   P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- Args.parse) --| P.$$$ ")") >> Args.src;
 
 val recdef_decl =
   Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
-  P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
+  P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
     -- Scan.option hints
   >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
 
 val _ =
   OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl

     (defer_recdef_decl >> Toplevel.theory);
 
 val _ =
   OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
     K.thy_goal
-    ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.xname --
+    ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.xname --
         Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
       >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
 
 end;