diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/raw_simplifier.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -306,7 +306,7 @@
   let
     val names = Term.declare_term_names t Name.context;
     val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
-    fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
+    fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_boundT (x', T));
   in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
 
 fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^