diff -r 9c4f4ac0d038 -r d8e4cd2ac2a1 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Thu Mar 05 08:23:10 2009 +0100
+++ b/src/HOL/UNITY/Union.thy	Thu Mar 05 08:23:11 2009 +0100
@@ -43,7 +43,7 @@
 translations
   "JN x : A. B"   == "JOIN A (%x. B)"
   "JN x y. B"   == "JN x. JN y. B"
-  "JN x. B"     == "JOIN UNIV (%x. B)"
+  "JN x. B"     == "JOIN CONST UNIV (%x. B)"
 
 syntax (xsymbols)
   SKIP     :: "'a program"                              ("\<bottom>")