
diff -r 3ee75fe01986 -r 00cd193a48dc src/HOL/HOLCF/Up.thy
--- a/src/HOL/HOLCF/Up.thy	Thu Jan 05 15:31:49 2012 +0100
+++ b/src/HOL/HOLCF/Up.thy	Thu Jan 05 18:18:39 2012 +0100
@@ -181,6 +181,7 @@
 
 translations
   "case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
+  "case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" => "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
   "\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
 
 text {* continuous versions of lemmas for @{typ "('a)u"} *}




