diff -r 48df747c8543 -r 6ea9de67e576 src/HOL/Library/Nested_Environment.thy
--- a/src/HOL/Library/Nested_Environment.thy	Tue Apr 22 08:33:13 2008 +0200
+++ b/src/HOL/Library/Nested_Environment.thy	Tue Apr 22 08:33:16 2008 +0200
@@ -527,20 +527,20 @@
 
 lemma [code func, code func del]:
   fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
-  shows "eq e1 e2 \<longleftrightarrow> eq e1 e2" ..
+  shows "eq_class.eq e1 e2 \<longleftrightarrow> eq_class.eq e1 e2" ..
 
 lemma eq_env_code [code func]:
   fixes x y :: "'a\<Colon>eq"
     and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"
-  shows "eq (Env x f) (Env y g) \<longleftrightarrow>
-  eq x y \<and> (\<forall>z\<in>UNIV. case f z
+  shows "eq_class.eq (Env x f) (Env y g) \<longleftrightarrow>
+  eq_class.eq x y \<and> (\<forall>z\<in>UNIV. case f z
    of None \<Rightarrow> (case g z
         of None \<Rightarrow> True | Some _ \<Rightarrow> False)
     | Some a \<Rightarrow> (case g z
-        of None \<Rightarrow> False | Some b \<Rightarrow> eq a b))" (is ?env)
-    and "eq (Val a) (Val b) \<longleftrightarrow> eq a b"
-    and "eq (Val a) (Env y g) \<longleftrightarrow> False"
-    and "eq (Env x f) (Val b) \<longleftrightarrow> False"
+        of None \<Rightarrow> False | Some b \<Rightarrow> eq_class.eq a b))" (is ?env)
+    and "eq_class.eq (Val a) (Val b) \<longleftrightarrow> eq_class.eq a b"
+    and "eq_class.eq (Val a) (Env y g) \<longleftrightarrow> False"
+    and "eq_class.eq (Env x f) (Val b) \<longleftrightarrow> False"
 proof (unfold eq)
   have "f = g \<longleftrightarrow> (\<forall>z. case f z
    of None \<Rightarrow> (case g z