diff -r 301b74fcd614 -r 92b9b8d2888d Nominal/nominal_eqvt.ML
--- a/Nominal/nominal_eqvt.ML	Sat Mar 17 05:13:59 2012 +0000
+++ b/Nominal/nominal_eqvt.ML	Tue Mar 20 11:26:10 2012 +0000
@@ -124,13 +124,11 @@
     fold_map note_named_thm (names ~~ thms) ctxt |> snd
   end
 
-local structure P = Parse and K = Keyword in
 
 val _ =
-  Outer_Syntax.local_theory "equivariance"
+  Outer_Syntax.local_theory ("equivariance", Keyword.thy_decl)
     "Proves equivariance for inductive predicate involving nominal datatypes." 
-      K.thy_decl (P.xname >> equivariance_cmd);
+      (Parse.xname >> equivariance_cmd)
 
-end;
 
 end (* structure *)