--- a/Nominal/Ex/Lambda.thy	Tue Apr 10 15:21:07 2012 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Apr 10 15:22:16 2012 +0100
@@ -7,6 +7,8 @@
 
 atom_decl name
 
+ML {* trace := true *}
+
 nominal_datatype lam =
   Var "name"
 | App "lam" "lam"
@@ -19,11 +21,11 @@
 lemma abs_lam_eqvt[eqvt]: "(p \<bullet> abs_lam t) = abs_lam (p \<bullet> t)"
 proof -
   have "alpha_lam_raw (rep_lam (abs_lam t)) t"
-    using rep_abs_rsp_left Quotient_lam equivp_reflp lam_equivp by metis
+    using rep_abs_rsp_left Quotient3_lam equivp_reflp lam_equivp by metis
   then have "alpha_lam_raw (p \<bullet> rep_lam (abs_lam t)) (p \<bullet> t)"
     unfolding alpha_lam_raw_eqvt[symmetric] permute_pure .
   then have "abs_lam (p \<bullet> rep_lam (abs_lam t)) = abs_lam (p \<bullet> t)"
-    using Quotient_rel Quotient_lam by metis
+    using Quotient3_rel Quotient3_lam by metis
   thus ?thesis using permute_lam_def id_apply map_fun_apply by metis
 qed