src/Pure/Syntax/syn_trans.ML

 
 
 (* 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;
 
 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
       if Term.loose_bvar1 (B, 0) then