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