--- 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 =
--- 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 []