# HG changeset patch
# User wenzelm
# Date 1004748285 -3600
# Node ID 0f6417c9a187cf3196a4f6276b620f30bef7eb40
# Parent  1b883fa9458ead2c5039df53282dc9fb6f05cf51
replaced Undef by UU;

diff -r 1b883fa9458e -r 0f6417c9a187 src/HOLCF/IMP/Denotational.thy
--- a/src/HOLCF/IMP/Denotational.thy	Sat Nov 03 01:44:26 2001 +0100
+++ b/src/HOLCF/IMP/Denotational.thy	Sat Nov 03 01:44:45 2001 +0100
@@ -10,7 +10,7 @@
 
 constdefs
    dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)"
-  "dlift f == (LAM x. case x of Undef => UU | Def(y) => f$(Discr y))"
+  "dlift f == (LAM x. case x of UU => UU | Def(y) => f$(Discr y))"
 
 consts D :: "com => state discr -> state lift"