--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Mon Jun 11 14:02:57 2012 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Tue Jun 12 01:23:52 2012 +0100
@@ -7,12 +7,12 @@
   CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)
 where
   "eqvt k \<Longrightarrow> (x~)*k = k (x~)"
-| "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Lam c (k (c~)))))))"
+| "eqvt k \<Longrightarrow> (M$$N)*k = M*(%m. (N*(%n.((m $$ n) $$ (Lam c (k (c~)))))))"
 | "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam c (M^(c~))))"
 | "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t"
-| "(x~)^l = l $ (x~)"
-| "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))"
-| "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $ (Lam x (Lam c (M^(c~))))"
+| "(x~)^l = l $$ (x~)"
+| "(M$$N)^l = M*(%m. (N*(%n.((m $$ n) $$ l))))"
+| "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))"
   apply (simp only: eqvt_def CPS1_CPS2_graph_def)
   apply (rule, perm_simp, rule)
   apply auto