diff -r 425b4c406d80 -r b3d97424b130 Nominal/Ex/CPS/CPS2_DanvyNielsen.thy
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Mon Jun 11 14:02:57 2012 +0100
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Tue Jun 12 01:23:52 2012 +0100
@@ -13,8 +13,8 @@
   fill   :: "cpsctxt \<Rightarrow> lt \<Rightarrow> lt"         ("_<_>" [200, 200] 100)
 where
   fill_hole : "Hole<M> = M"
-| fill_fun  : "(CFun C N)<M> = (C<M>) $ N"
-| fill_arg  : "(CArg N C)<M> = N $ (C<M>)"
+| fill_fun  : "(CFun C N)<M> = (C<M>) $$ N"
+| fill_arg  : "(CArg N C)<M> = N $$ (C<M>)"
 | fill_abs  : "atom x \<sharp> M \<Longrightarrow> (CAbs x C)<M> = Lam x (C<M>)"
   unfolding eqvt_def fill_graph_def
   apply perm_simp
@@ -64,14 +64,14 @@
 | "CPS (Var x) = CFun Hole (x~)"
 | "atom b \<sharp> M \<Longrightarrow> CPSv (Lam y M) = Lam y (Lam b ((CPS M)<Var b>))"
 | "atom b \<sharp> M \<Longrightarrow> CPS (Lam y M) = CFun Hole (Lam y (Lam b ((CPS M)<Var b>)))"
-| "CPSv (M $ N) = Lam x (Var x)"
-| "isValue M \<Longrightarrow> isValue N \<Longrightarrow> CPS (M $ N) = CArg (CPSv M $ CPSv N) Hole"
-| "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> M \<Longrightarrow> CPS (M $ N) =
-     ccomp (CPS N) (CAbs a (CArg (CPSv M $ Var a) Hole))"
-| "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) =
-     ccomp (CPS M) (CAbs a (CArg (Var a $ (CPSv N)) Hole))"
-| "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $ N) =
-     ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $ Var b) Hole))))"
+| "CPSv (M $$ N) = Lam x (Var x)"
+| "isValue M \<Longrightarrow> isValue N \<Longrightarrow> CPS (M $$ N) = CArg (CPSv M $$ CPSv N) Hole"
+| "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> M \<Longrightarrow> CPS (M $$ N) =
+     ccomp (CPS N) (CAbs a (CArg (CPSv M $$ Var a) Hole))"
+| "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $$ N) =
+     ccomp (CPS M) (CAbs a (CArg (Var a $$ (CPSv N)) Hole))"
+| "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $$ N) =
+     ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $$ Var b) Hole))))"
   apply auto
   defer
   apply (case_tac x)