# HG changeset patch
# User haftmann
# Date 1393412275 -3600
# Node ID 385f7573f8f5b5ccebc9d05f4b3598fd56ef91bb
# Parent  9fc71814b8c183afe24d7fcfc5dcddfafe658cf8
obsolete workaround

diff -r 9fc71814b8c1 -r 385f7573f8f5 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