diff -r 132575f5bd26 -r f0fab367453a Nominal/Ex/CPS/CPS2_DanvyNielsen.thy
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Fri Aug 19 11:07:17 2011 +0900
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Fri Aug 19 12:49:38 2011 +0900
@@ -7,7 +7,7 @@
   Hole
 | CFun cpsctxt lt
 | CArg lt cpsctxt
-| CAbs x::name c::cpsctxt bind x in c
+| CAbs x::name c::cpsctxt binds x in c
 
 nominal_primrec
   fill   :: "cpsctxt \<Rightarrow> lt \<Rightarrow> lt"         ("_<_>" [200, 200] 100)
@@ -15,7 +15,7 @@
   fill_hole : "Hole<M> = 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> = Abs x (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
   apply auto
@@ -29,11 +29,7 @@
   apply (simp add: eqvt_at_def swap_fresh_fresh)
   done
 
-termination
-  by (relation "measure (\<lambda>(x, _). size x)") (auto simp add: cpsctxt.size)
-
-lemma [eqvt]: "p \<bullet> fill c t = fill (p \<bullet> c) (p \<bullet> t)"
-  by (nominal_induct c avoiding: t rule: cpsctxt.strong_induct) simp_all
+termination (eqvt) by lexicographic_order
 
 nominal_primrec
   ccomp :: "cpsctxt => cpsctxt => cpsctxt"
@@ -56,20 +52,16 @@
   apply (simp add: eqvt_at_def swap_fresh_fresh)
   done
 
-termination
-  by (relation "measure (\<lambda>(x, _). size x)") (auto simp add: cpsctxt.size)
-
-lemma [eqvt]: "p \<bullet> ccomp c c' = ccomp (p \<bullet> c) (p \<bullet> c')"
-  by (nominal_induct c avoiding: c' rule: cpsctxt.strong_induct) simp_all
+termination (eqvt) by lexicographic_order
 
 nominal_primrec
     CPSv :: "lt => lt"
 and CPS :: "lt => cpsctxt" where
   "CPSv (Var x) = x~"
 | "CPS (Var x) = CFun Hole (x~)"
-| "atom b \<sharp> M \<Longrightarrow> CPSv (Abs y M) = Abs y (Abs b ((CPS M)<Var b>))"
-| "atom b \<sharp> M \<Longrightarrow> CPS (Abs y M) = CFun Hole (Abs y (Abs b ((CPS M)<Var b>)))"
-| "CPSv (M $ N) = Abs x (Var 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))"
@@ -97,8 +89,8 @@
   apply (simp_all add: fresh_Pair)[4]
 --""
   apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "Abs b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Abs a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)")
-  apply (subgoal_tac "Abs ba (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Abs a (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)")
+  apply (subgoal_tac "Lam b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)")
+  apply (subgoal_tac "Lam ba (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)")
   apply (simp only:)
   apply (erule Abs_lst1_fcb)
   apply (simp add: Abs_fresh_iff)