src/Pure/codegen.ML

   let val {preprocs, ...} = CodegenData.get thy
   in fold (fn (_, f) => f thy) preprocs end;
 
 fun preprocess_term thy t =
   let
-    val x = Free (Name.variant (OldTerm.add_term_names (t, [])) "x", fastype_of t);
+    val x = Free (singleton (Name.variant_list (OldTerm.add_term_names (t, []))) "x", fastype_of t);
     (* fake definition *)
     val eq = Skip_Proof.make_thm thy (Logic.mk_equals (x, t));
     fun err () = error "preprocess_term: bad preprocessor"
   in case map prop_of (preprocess thy [eq]) of
       [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()