obsolete workaround
authorhaftmann
Wed, 26 Feb 2014 11:57:55 +0100
changeset 55758 385f7573f8f5
parent 55757 9fc71814b8c1
child 55759 fe3d8f585c20
obsolete workaround
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