--- a/Nominal/nominal_function.ML	Fri May 16 08:38:23 2014 +0100
+++ b/Nominal/nominal_function.ML	Mon May 19 11:19:48 2014 +0100
@@ -181,7 +181,7 @@
           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
           fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts}
 
-        val _ = Proof_Display.print_consts do_print 
+        val _ = Proof_Display.print_consts do_print
           (Position.thread_data ()) lthy (K false) (map fst fixes)
       in
         (info, 
@@ -265,7 +265,7 @@
      || ((Parse.reserved "invariant" |-- Parse.term) >> Invariant))
 
   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 nominal_function_parser default_cfg =