--- a/Nominal/nominal_termination.ML	Sat Mar 17 05:13:59 2012 +0000
+++ b/Nominal/nominal_termination.ML	Tue Mar 20 11:26:10 2012 +0000
@@ -101,15 +101,15 @@
 (* outer syntax *)
 
 val option_parser =
-  (Scan.optional (Parse.$$$ "(" |-- Parse.!!! 
+  (Scan.optional (@{keyword "("} |-- Parse.!!! 
     ((Parse.reserved "eqvt" >> K (true, true)) ||
-     (Parse.reserved "no_eqvt" >> K (true, false))) --| Parse.$$$ ")") (false, false))
+     (Parse.reserved "no_eqvt" >> K (true, false))) --| @{keyword ")"}) (false, false))
 
 val _ =
-  Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function"
-  Keyword.thy_goal
-  (option_parser -- Scan.option Parse.term >> 
-     (fn ((is_nominal, is_eqvt), opt_trm) => 
-        if is_nominal then termination_cmd is_eqvt opt_trm else Function.termination_cmd opt_trm))
+  Outer_Syntax.local_theory_to_proof ("termination", Keyword.thy_goal) 
+    "prove termination of a recursive function"
+      (option_parser -- Scan.option Parse.term >> 
+        (fn ((is_nominal, is_eqvt), opt_trm) => 
+           if is_nominal then termination_cmd is_eqvt opt_trm else Function.termination_cmd opt_trm))
 
 end