--- a/src/HOL/Library/OptionalSugar.thy Sat Feb 20 23:23:04 2010 +0100
+++ b/src/HOL/Library/OptionalSugar.thy Sun Feb 21 20:53:50 2010 +0100
@@ -37,15 +37,15 @@
(* Let *)
translations
- "_bind (p,DUMMY) e" <= "_bind p (CONST fst e)"
- "_bind (DUMMY,p) e" <= "_bind p (CONST snd e)"
+ "_bind (p, CONST DUMMY) e" <= "_bind p (CONST fst e)"
+ "_bind (CONST 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 (CONST the e)"
- "_bind (p#DUMMY) e" <= "_bind p (CONST hd e)"
- "_bind (DUMMY#p) e" <= "_bind p (CONST tl e)"
+ "_bind (CONST Some p) e" <= "_bind p (CONST the e)"
+ "_bind (p # CONST DUMMY) e" <= "_bind p (CONST hd e)"
+ "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
(* type constraints with spacing *)
setup {*