--- a/src/HOL/Tools/code_evaluation.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/HOL/Tools/code_evaluation.ML Thu Jun 09 20:22:22 2011 +0200
@@ -57,7 +57,7 @@
fun mk_term_of_eq thy ty (c, (_, tys)) =
let
val t = list_comb (Const (c, tys ---> ty),
- map Free (Name.names Name.context "a" tys));
+ map Free (Name.invent_names Name.context "a" tys));
val (arg, rhs) =
pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
(t, (map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)