--- 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;