src/HOL/Tools/recdef_package.ML

 local structure P = OuterParse and K = OuterKeyword in
 
 val _ = List.app OuterKeyword.keyword ["permissive", "congs", "hints"];
 
 val hints =
-  P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
+  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 ":" -- P.prop) -- Scan.option hints
   >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);