src/HOLCF/IMP/Denotational.thy
changeset 12032 0f6417c9a187
parent 10835 f4745d77e620
child 12338 de0f4a63baa5
--- 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"