diff -r 682dfb674df3 -r 6f306c8c2c54 src/HOL/Library/Nested_Environment.thy
--- a/src/HOL/Library/Nested_Environment.thy	Wed Apr 02 15:58:31 2008 +0200
+++ b/src/HOL/Library/Nested_Environment.thy	Wed Apr 02 15:58:32 2008 +0200
@@ -527,21 +527,21 @@
 
 lemma [code func, code func del]:
   fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
-  shows "e1 = e2 \<longleftrightarrow> e1 = e2" ..
+  shows "eq e1 e2 \<longleftrightarrow> 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 "Env x f = Env y g \<longleftrightarrow>
-  x = y \<and> (\<forall>z\<in>UNIV. case f z
+  shows "eq (Env x f) (Env y g) \<longleftrightarrow>
+  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> a = b))" (is ?env)
-    and "Val a = Val b \<longleftrightarrow> a = b"
-    and "Val a = Env y g \<longleftrightarrow> False"
-    and "Env x f = Val b \<longleftrightarrow> False"
-proof -
+        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"
+proof (unfold eq)
   have "f = g \<longleftrightarrow> (\<forall>z. case f z
    of None \<Rightarrow> (case g z
         of None \<Rightarrow> True | Some _ \<Rightarrow> False)
@@ -559,7 +559,12 @@
       then show "f z = g z" by (auto split: option.splits)
     qed
   qed
-  then show ?env by simp
+  then show "Env x f = Env y g \<longleftrightarrow>
+    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> a = b))" by simp
 qed simp_all
 
 end