# HG changeset patch
# User wenzelm
# Date 1365623188 -7200
# Node ID 1eb533ea148059a711bc0ae59cef7c19ce2040f1
# Parent  ecd34f8632421272691c6080e40200e4f44bdc19
more antiquotations;

diff -r ecd34f863242 -r 1eb533ea1480 src/HOL/Hoare/hoare_syntax.ML
--- a/src/HOL/Hoare/hoare_syntax.ML	Wed Apr 10 21:20:35 2013 +0200
+++ b/src/HOL/Hoare/hoare_syntax.ML	Wed Apr 10 21:46:28 2013 +0200
@@ -18,7 +18,7 @@
 local
 
 fun idt_name (Free (x, _)) = SOME x
-  | idt_name (Const ("_constrain", _) $ t $ _) = idt_name t
+  | idt_name (Const (@{syntax_const "_constrain"}, _) $ t $ _) = idt_name t
   | idt_name _ = NONE;
 
 fun eq_idt tu =
diff -r ecd34f863242 -r 1eb533ea1480 src/HOL/Tools/case_translation.ML
--- a/src/HOL/Tools/case_translation.ML	Wed Apr 10 21:20:35 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Wed Apr 10 21:46:28 2013 +0200
@@ -110,7 +110,8 @@
         fun abs p tTs t = Syntax.const @{const_syntax case_abs} $
           fold constrain_Abs tTs (absfree p t);
 
-        fun abs_pat (Const ("_constrain", _) $ t $ tT) tTs = abs_pat t (tT :: tTs)
+        fun abs_pat (Const (@{syntax_const "_constrain"}, _) $ t $ tT) tTs =
+              abs_pat t (tT :: tTs)
           | abs_pat (Free (p as (x, _))) tTs =
               if is_const x then I else abs p tTs
           | abs_pat (t $ u) _ = abs_pat u [] #> abs_pat t []