--- a/Nominal/nominal_inductive.ML	Sat Mar 17 05:13:59 2012 +0000
+++ b/Nominal/nominal_inductive.ML	Tue Mar 20 11:26:10 2012 +0000
@@ -420,23 +420,19 @@
 
 (* outer syntax *)
 local
-  structure P = Parse;
-  structure S = Scan
-  
-  val _ = Keyword.keyword "avoids"
 
   val single_avoid_parser = 
-    P.name -- (P.$$$ ":" |-- P.and_list1 P.term)
+    Parse.name -- (@{keyword ":"} |-- Parse.and_list1 Parse.term)
 
   val avoids_parser = 
-    S.optional (P.$$$ "avoids" |-- P.enum1 "|" single_avoid_parser) []
+    Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" single_avoid_parser) []
 
-  val main_parser = P.xname -- avoids_parser
+  val main_parser = Parse.xname -- avoids_parser
 in
   val _ =
-  Outer_Syntax.local_theory_to_proof "nominal_inductive"
-    "prove strong induction theorem for inductive predicate involving nominal datatypes"
-      Keyword.thy_goal (main_parser >> prove_strong_inductive_cmd)
+    Outer_Syntax.local_theory_to_proof ("nominal_inductive", Keyword.thy_goal)
+      "prove strong induction theorem for inductive predicate involving nominal datatypes"
+        (main_parser >> prove_strong_inductive_cmd)
 end
 
 end