src/HOL/Tools/Function/function_common.ML
changeset 46949 94aa7b81bcf6
parent 46496 b8920f3fd259
child 49965 ee25a04fa06a
--- 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 =