src/HOL/Orderings.thy
changeset 35364 b8c62d60195c
parent 35301 90e42f9ba4d1
child 35579 cc9a5a0ab5ea
     1.1 --- a/src/HOL/Orderings.thy	Thu Feb 25 22:17:33 2010 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Thu Feb 25 22:32:09 2010 +0100
     1.3 @@ -657,13 +657,14 @@
     1.4  
     1.5    fun matches_bound v t =
     1.6      (case t of
     1.7 -      Const ("_bound", _) $ Free (v', _) => v = v'
     1.8 +      Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v'
     1.9      | _ => false);
    1.10    fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
    1.11    fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P;
    1.12  
    1.13    fun tr' q = (q,
    1.14 -    fn [Const ("_bound", _) $ Free (v, _), Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
    1.15 +    fn [Const (@{syntax_const "_bound"}, _) $ Free (v, _),
    1.16 +        Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
    1.17          (case AList.lookup (op =) trans (q, c, d) of
    1.18            NONE => raise Match
    1.19          | SOME (l, g) =>