diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/Classical.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -67,7 +67,7 @@
           (if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)"
 | "atom a \<sharp> (d, e) \<Longrightarrow> (ImpL <a>.M (x).N y)[d\<turnstile>c>e] = ImpL <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e]) y"
   apply(simp only: eqvt_def)
-  apply(simp only: crename_graph_def)
+  apply(simp only: crename_graph_aux_def)
   apply (rule, perm_simp, rule)
   apply(rule TrueI)
   -- "covered all cases"
@@ -272,7 +272,7 @@
 | "atom x \<sharp> (u, v) \<Longrightarrow> (ImpL <a>.M (x).N y)[u\<turnstile>n>v] = 
         (if y=u then ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) v else ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) y)"
   apply(simp only: eqvt_def)
-  apply(simp only: nrename_graph_def)
+  apply(simp only: nrename_graph_aux_def)
   apply (rule, perm_simp, rule)
   apply(rule TrueI)
   -- "covered all cases"
@@ -474,7 +474,7 @@
      (if y=z then Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z' 
       else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)"
   apply(simp only: eqvt_def)
-  apply(simp only: substn_graph_def)
+  apply(simp only: substn_graph_aux_def)
   apply (rule, perm_simp, rule)
   apply(rule TrueI)
   -- "covered all cases"