diff -r a5dc3558cdec -r ce0255ffaeb4 Nominal-General/nominal_eqvt.ML
--- a/Nominal-General/nominal_eqvt.ML	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal-General/nominal_eqvt.ML	Fri May 21 10:42:53 2010 +0200
@@ -184,10 +184,10 @@
   equivariance preds raw_induct intrs ctxt |> snd
 end
 
-local structure P = OuterParse and K = OuterKeyword in
+local structure P = Parse and K = Keyword in
 
 val _ =
-  OuterSyntax.local_theory "equivariance"
+  Outer_Syntax.local_theory "equivariance"
     "Proves equivariance for inductive predicate involving nominal datatypes." 
       K.thy_decl (P.xname >> equivariance_cmd);
 end;