TFL/usyntax.ML

 fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
   | dest_comb _ =  raise USYN_ERR "dest_comb" "not a comb";
 
 fun dest_abs used (a as Abs(s, ty, M)) =
      let
-       val s' = variant used s;
+       val s' = Name.variant used s;
        val v = Free(s', ty);
      in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
      end
   | dest_abs _ _ =  raise USYN_ERR "dest_abs" "not an abstraction";