--- a/src/HOL/Metis_Examples/Message.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Metis_Examples/Message.thy Mon Feb 08 21:28:27 2010 +0100
@@ -52,7 +52,7 @@
translations
"{|x, y, z|}" == "{|x, {|y, z|}|}"
- "{|x, y|}" == "MPair x y"
+ "{|x, y|}" == "CONST MPair x y"
constdefs