diff -r 14c7d7e29c44 -r 87d1e815aa59 Nominal/nominal_eqvt.ML
--- a/Nominal/nominal_eqvt.ML	Sun Jul 15 13:03:47 2012 +0100
+++ b/Nominal/nominal_eqvt.ML	Fri Aug 03 14:46:25 2012 +0200
@@ -126,7 +126,7 @@
 
 
 val _ =
-  Outer_Syntax.local_theory ("equivariance", Keyword.thy_decl)
+  Outer_Syntax.local_theory @{command_spec "equivariance"}
     "Proves equivariance for inductive predicate involving nominal datatypes." 
       (Parse.xname >> equivariance_cmd)