diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/CPS/Lt.thy
--- a/Nominal/Ex/CPS/Lt.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/CPS/Lt.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -16,7 +16,7 @@
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
-  unfolding eqvt_def subst_graph_def
+  unfolding eqvt_def subst_graph_aux_def
   apply (simp)
   apply(rule TrueI)
   using [[simproc del: alpha_lst]]
@@ -51,8 +51,8 @@
   "isValue (Var x) = True"
 | "isValue (Lam y N) = True"
 | "isValue (A $$ B) = False"
-  unfolding eqvt_def isValue_graph_def
-  by (perm_simp, auto)
+  unfolding eqvt_def isValue_graph_aux_def
+  by (auto)
      (erule lt.exhaust, auto)
 
 termination (eqvt)