src/Pure/Syntax/syn_trans.ML

--- a/src/Pure/Syntax/syn_trans.ML	Tue Jul 11 12:17:00 2006 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Tue Jul 11 12:17:01 2006 +0200
@@ -384,7 +384,7 @@
 (* dependent / nondependent quantifiers *)
 
 fun variant_abs' (x, T, B) =
-  let val x' = variant (add_term_names (B, [])) x in
+  let val x' = Name.variant (add_term_names (B, [])) x in
     (x', subst_bound (mark_boundT (x', T), B))
   end;