src/HOL/Hoare/hoare_syntax.ML
changeset 51693 1eb533ea1480
parent 42284 326f57825e1a
child 55414 eab03e9cee8a
     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 =