src/HOL/Orderings.thy
changeset 42284 326f57825e1a
parent 41082 9ff94e7cc3b3
child 42287 d98eb048a2e4
--- 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, _),