src/HOL/Tools/inductive_codegen.ML

     else ps
   end;
 
 fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of
       NONE => ((names, (s, [s])::vs), s)
-    | SOME xs => let val s' = variant names s in
+    | SOME xs => let val s' = Name.variant names s in
         ((s'::names, AList.update (op =) (s, s'::xs) vs), s') end);
 
 fun distinct_v (nvs, Var ((s, 0), T)) =
       apsnd (Var o rpair T o rpair 0) (mk_v (nvs, s))
   | distinct_v (nvs, t $ u) =

       (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
         (arg_vs ~~ iss);
 
     fun check_constrt ((names, eqs), t) =
       if is_constrt thy t then ((names, eqs), t) else
-        let val s = variant names "x";
+        let val s = Name.variant names "x";
         in ((s::names, (s, t)::eqs), Var ((s, 0), fastype_of t)) end;
 
     fun compile_eq (gr, (s, t)) =
       apsnd (Pretty.block o cons (Pretty.str (s ^ " = ")) o single)
         (invoke_codegen thy defs dep module false (gr, t));