# HG changeset patch
# User wenzelm
# Date 1266782030 -3600
# Node ID 92664dca6f20ea2822f6243416efef7a3d0166e5
# Parent  7024a8a8f36a8161f1b9371f799942b43549d54c
proper markup of const syntax;

diff -r 7024a8a8f36a -r 92664dca6f20 src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Sat Feb 20 23:23:04 2010 +0100
+++ b/src/HOL/Import/hol4rews.ML	Sun Feb 21 20:53:50 2010 +0100
@@ -613,13 +613,13 @@
     end
 
 local
-    fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==", _],_,_]] = x
-      | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "all", _],_]] = x
-      | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==>", _],_,_]] = x
+    fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "=="}, _],_,_]] = x
+      | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax all}, _],_]] = x
+      | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "==>"}, _],_,_]] = x
       | handle_meta [x] = Appl[Constant "Trueprop",x]
       | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
 in
-val smarter_trueprop_parsing = [("Trueprop",handle_meta)]
+val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)]
 end
 
 local
diff -r 7024a8a8f36a -r 92664dca6f20 src/HOL/Library/OptionalSugar.thy
--- 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 {*