--- a/src/HOL/Tools/Function/function_common.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Function/function_common.ML Thu Mar 15 20:07:00 2012 +0100
@@ -345,7 +345,7 @@
|| (Parse.reserved "no_partials" >> K No_Partials))
fun config_parser default =
- (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
+ (Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) [])
>> (fn opts => fold apply_opt opts default)
in
fun function_parser default_cfg =