1.1 --- a/src/HOL/Library/OptionalSugar.thy	Mon Mar 09 23:07:51 2009 +0100
     1.2 +++ b/src/HOL/Library/OptionalSugar.thy	Tue Mar 10 10:59:59 2009 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  (* set *)
     1.6  translations
     1.7 -  "xs" <= "set xs"
     1.8 +  "xs" <= "CONST set xs"
     1.9  
    1.10  (* append *)
    1.11  syntax (latex output)
    1.12 @@ -26,15 +26,15 @@
    1.13  
    1.14  (* Let *)
    1.15  translations 
    1.16 -  "_bind (p,DUMMY) e" <= "_bind p (fst e)"
    1.17 -  "_bind (DUMMY,p) e" <= "_bind p (snd e)"
    1.18 +  "_bind (p,DUMMY) e" <= "_bind p (CONST fst e)"
    1.19 +  "_bind (DUMMY,p) e" <= "_bind p (CONST snd e)"
    1.20  
    1.21    "_tuple_args x (_tuple_args y z)" ==
    1.22      "_tuple_args x (_tuple_arg (_tuple y z))"
    1.23  
    1.24 -  "_bind (Some p) e" <= "_bind p (the e)"
    1.25 -  "_bind (p#DUMMY) e" <= "_bind p (hd e)"
    1.26 -  "_bind (DUMMY#p) e" <= "_bind p (tl e)"
    1.27 +  "_bind (Some p) e" <= "_bind p (CONST the e)"
    1.28 +  "_bind (p#DUMMY) e" <= "_bind p (CONST hd e)"
    1.29 +  "_bind (DUMMY#p) e" <= "_bind p (CONST tl e)"
    1.30  
    1.31  (* type constraints with spacing *)
    1.32  setup {*