more antiquotations;
authorwenzelm
Wed Apr 10 21:46:28 2013 +0200 (2013-04-10)
changeset 516931eb533ea1480
parent 51692 ecd34f863242
child 51694 6ae88642962f
more antiquotations;
src/HOL/Hoare/hoare_syntax.ML
src/HOL/Tools/case_translation.ML
     1.1 --- a/src/HOL/Hoare/hoare_syntax.ML	Wed Apr 10 21:20:35 2013 +0200
     1.2 +++ b/src/HOL/Hoare/hoare_syntax.ML	Wed Apr 10 21:46:28 2013 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  local
     1.5  
     1.6  fun idt_name (Free (x, _)) = SOME x
     1.7 -  | idt_name (Const ("_constrain", _) $ t $ _) = idt_name t
     1.8 +  | idt_name (Const (@{syntax_const "_constrain"}, _) $ t $ _) = idt_name t
     1.9    | idt_name _ = NONE;
    1.10  
    1.11  fun eq_idt tu =
     2.1 --- a/src/HOL/Tools/case_translation.ML	Wed Apr 10 21:20:35 2013 +0200
     2.2 +++ b/src/HOL/Tools/case_translation.ML	Wed Apr 10 21:46:28 2013 +0200
     2.3 @@ -110,7 +110,8 @@
     2.4          fun abs p tTs t = Syntax.const @{const_syntax case_abs} $
     2.5            fold constrain_Abs tTs (absfree p t);
     2.6  
     2.7 -        fun abs_pat (Const ("_constrain", _) $ t $ tT) tTs = abs_pat t (tT :: tTs)
     2.8 +        fun abs_pat (Const (@{syntax_const "_constrain"}, _) $ t $ tT) tTs =
     2.9 +              abs_pat t (tT :: tTs)
    2.10            | abs_pat (Free (p as (x, _))) tTs =
    2.11                if is_const x then I else abs p tTs
    2.12            | abs_pat (t $ u) _ = abs_pat u [] #> abs_pat t []