diff -r 5818d9cfb2e7 -r 644b62cf678f src/HOLCF/IOA/meta_theory/TL.thy
--- a/src/HOLCF/IOA/meta_theory/TL.thy	Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/TL.thy	Tue Oct 07 16:07:50 2008 +0200
@@ -38,9 +38,7 @@
 defs
 
 unlift_def:
-  "unlift x == (case x of
-                 UU   => arbitrary
-               | Def y   => y)"
+  "unlift x == (case x of Def y   => y)"
 
 (* this means that for nil and UU the effect is unpredictable *)
 Init_def: