diff -r 25d9d836ed9c -r 326f57825e1a src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -688,7 +688,7 @@
       pair (IVar (SOME v))
   | translate_term thy algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
       let
-        val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t);
+        val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize false v, ty, t);
         val v'' = if member (op =) (Term.add_free_names t' []) v'
           then SOME v' else NONE
       in