diff -r abf147627b4b -r a303ef51cd97 Nominal/Ex/BetaCR.thy
--- a/Nominal/Ex/BetaCR.thy	Mon Dec 19 16:39:20 2011 +0900
+++ b/Nominal/Ex/BetaCR.thy	Tue Dec 20 11:40:04 2011 +0900
@@ -243,7 +243,7 @@
 quotient_definition "QVar::name \<Rightarrow> qlam" is Var
 quotient_definition "QApp::qlam \<Rightarrow> qlam \<Rightarrow> qlam" is App
 quotient_definition QLam ("QLam [_]._")
-  where "QLam::name \<Rightarrow> qlam \<Rightarrow> qlam" is Beta.Lam
+  where "QLam::name \<Rightarrow> qlam \<Rightarrow> qlam" is BetaCR.Lam
 
 lemmas qlam_strong_induct = lam.strong_induct[quot_lifted]
 lemmas qlam_induct = lam.induct[quot_lifted]