src/HOL/Library/OptionalSugar.thy
changeset 35250 92664dca6f20
parent 35115 446c5063e4fd
child 38864 4abe644fcea5
     1.1 --- a/src/HOL/Library/OptionalSugar.thy	Sat Feb 20 23:23:04 2010 +0100
     1.2 +++ b/src/HOL/Library/OptionalSugar.thy	Sun Feb 21 20:53:50 2010 +0100
     1.3 @@ -37,15 +37,15 @@
     1.4  
     1.5  (* Let *)
     1.6  translations 
     1.7 -  "_bind (p,DUMMY) e" <= "_bind p (CONST fst e)"
     1.8 -  "_bind (DUMMY,p) e" <= "_bind p (CONST snd e)"
     1.9 +  "_bind (p, CONST DUMMY) e" <= "_bind p (CONST fst e)"
    1.10 +  "_bind (CONST DUMMY, p) e" <= "_bind p (CONST snd e)"
    1.11  
    1.12    "_tuple_args x (_tuple_args y z)" ==
    1.13      "_tuple_args x (_tuple_arg (_tuple y z))"
    1.14  
    1.15 -  "_bind (Some p) e" <= "_bind p (CONST the e)"
    1.16 -  "_bind (p#DUMMY) e" <= "_bind p (CONST hd e)"
    1.17 -  "_bind (DUMMY#p) e" <= "_bind p (CONST tl e)"
    1.18 +  "_bind (CONST Some p) e" <= "_bind p (CONST the e)"
    1.19 +  "_bind (p # CONST DUMMY) e" <= "_bind p (CONST hd e)"
    1.20 +  "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
    1.21  
    1.22  (* type constraints with spacing *)
    1.23  setup {*