--- 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]