diff -r 425b4c406d80 -r b3d97424b130 Nominal/Ex/CPS/Lt.thy
--- a/Nominal/Ex/CPS/Lt.thy	Mon Jun 11 14:02:57 2012 +0100
+++ b/Nominal/Ex/CPS/Lt.thy	Tue Jun 12 01:23:52 2012 +0100
@@ -7,7 +7,7 @@
 
 nominal_datatype lt =
     Var name       ("_~"  [150] 149)
-  | App lt lt         (infixl "$" 100)
+  | App lt lt         (infixl "$$" 100)
   | Lam x::"name" t::"lt"  binds  x in t
 
 nominal_primrec
@@ -49,7 +49,7 @@
 where
   "isValue (Var x) = True"
 | "isValue (Lam y N) = True"
-| "isValue (A $ B) = False"
+| "isValue (A $$ B) = False"
   unfolding eqvt_def isValue_graph_def
   by (perm_simp, auto)
      (erule lt.exhaust, auto)
@@ -60,9 +60,9 @@
 inductive
   eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
   where
-   evbeta: "\<lbrakk>atom x\<sharp>V; isValue V\<rbrakk> \<Longrightarrow> ((Lam x M) $ V) \<longrightarrow>\<^isub>\<beta> (M[x ::= V])"
-|  ev1: "\<lbrakk>isValue V; M \<longrightarrow>\<^isub>\<beta> M' \<rbrakk> \<Longrightarrow> (V $ M) \<longrightarrow>\<^isub>\<beta> (V $ M')"
-|  ev2: "M \<longrightarrow>\<^isub>\<beta> M' \<Longrightarrow> (M $ N) \<longrightarrow>\<^isub>\<beta> (M' $ N)"
+   evbeta: "\<lbrakk>atom x\<sharp>V; isValue V\<rbrakk> \<Longrightarrow> ((Lam x M) $$ V) \<longrightarrow>\<^isub>\<beta> (M[x ::= V])"
+|  ev1: "\<lbrakk>isValue V; M \<longrightarrow>\<^isub>\<beta> M' \<rbrakk> \<Longrightarrow> (V $$ M) \<longrightarrow>\<^isub>\<beta> (V $$ M')"
+|  ev2: "M \<longrightarrow>\<^isub>\<beta> M' \<Longrightarrow> (M $$ N) \<longrightarrow>\<^isub>\<beta> (M' $$ N)"
 
 equivariance eval
 
@@ -111,7 +111,7 @@
 lemma evbeta':
   fixes x :: name
   assumes "isValue V" and "atom x\<sharp>V" and "N = (M[x ::= V])"
-  shows "((Lam x M) $ V) \<longrightarrow>\<^isub>\<beta>\<^sup>* N"
+  shows "((Lam x M) $$ V) \<longrightarrow>\<^isub>\<beta>\<^sup>* N"
   using assms by simp (rule evs2, rule evbeta, simp_all add: evs1)
 
 end