1.1 --- a/src/HOL/Orderings.thy	Fri Apr 08 11:39:45 2011 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Apr 08 13:31:16 2011 +0200
     1.3 @@ -660,7 +660,7 @@
     1.4        Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v'
     1.5      | _ => false);
     1.6    fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
     1.7 -  fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P;
     1.8 +  fun mk v c n P = Syntax.const c $ Syntax_Trans.mark_bound v $ n $ P;
     1.9  
    1.10    fun tr' q = (q,
    1.11      fn [Const (@{syntax_const "_bound"}, _) $ Free (v, _),