src/HOL/Unix/Nested_Environment.thy

--- a/src/HOL/Unix/Nested_Environment.thy	Wed Feb 26 11:57:52 2014 +0100
+++ b/src/HOL/Unix/Nested_Environment.thy	Wed Feb 26 11:57:55 2014 +0100
@@ -563,9 +563,4 @@
 lemma [code nbe]: "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True"
   by (fact equal_refl)
 
-lemma [code, code del]:
-  "(Code_Evaluation.term_of ::
-    ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) =
-      Code_Evaluation.term_of" ..
-
 end