# HG changeset patch
# User wenzelm
# Date 1236679199 -3600
# Node ID d03dd6301678fd0993448ddc1c0f5b42070cd191
# Parent  c47e0189013b4f1650bc3974a610d0ef990fd2dc
more robust treatment of (authentic) consts within translations;

diff -r c47e0189013b -r d03dd6301678 src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Mon Mar 09 23:07:51 2009 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Tue Mar 10 10:59:59 2009 +0100
@@ -9,7 +9,7 @@
 
 (* set *)
 translations
-  "xs" <= "set xs"
+  "xs" <= "CONST set xs"
 
 (* append *)
 syntax (latex output)
@@ -26,15 +26,15 @@
 
 (* Let *)
 translations 
-  "_bind (p,DUMMY) e" <= "_bind p (fst e)"
-  "_bind (DUMMY,p) e" <= "_bind p (snd e)"
+  "_bind (p,DUMMY) e" <= "_bind p (CONST fst e)"
+  "_bind (DUMMY,p) e" <= "_bind p (CONST snd e)"
 
   "_tuple_args x (_tuple_args y z)" ==
     "_tuple_args x (_tuple_arg (_tuple y z))"
 
-  "_bind (Some p) e" <= "_bind p (the e)"
-  "_bind (p#DUMMY) e" <= "_bind p (hd e)"
-  "_bind (DUMMY#p) e" <= "_bind p (tl e)"
+  "_bind (Some p) e" <= "_bind p (CONST the e)"
+  "_bind (p#DUMMY) e" <= "_bind p (CONST hd e)"
+  "_bind (DUMMY#p) e" <= "_bind p (CONST tl e)"
 
 (* type constraints with spacing *)
 setup {*