diff -r b84688dd7f6b -r 1ca1142e1711 src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Wed Dec 09 16:22:29 2015 +0100
+++ b/src/HOL/Library/old_recdef.ML	Wed Dec 09 16:36:26 2015 +0100
@@ -2873,8 +2873,7 @@
 
 val hints =
   @{keyword "("} |--
-    Parse.!!! (Parse.position @{keyword "hints"} -- Parse.args --| @{keyword ")"})
-  >> uncurry Token.src;
+    Parse.!!! ((Parse.token @{keyword "hints"} ::: Parse.args) --| @{keyword ")"});
 
 val recdef_decl =
   Scan.optional