Nominal-General/nominal_eqvt.ML
changeset 2168 ce0255ffaeb4
parent 2117 b3a5bda07007
child 2306 86c977b4a9bb
--- 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;