# HG changeset patch
# User berghofe
# Date 1060271210 -7200
# Node ID ca089b9d13c476daa6a100b64a3f3cdf9c7af5ba
# Parent  ca3dd7ed5ac52806488332c7dec26c7e0cae9302
test_term now renames variable for size of test data to avoid clashes
with variables already present in the term to be tested.

diff -r ca3dd7ed5ac5 -r ca089b9d13c4 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue Aug 05 17:57:39 2003 +0200
+++ b/src/Pure/codegen.ML	Thu Aug 07 17:46:50 2003 +0200
@@ -554,17 +554,18 @@
       "Term to be tested contains schematic variables";
     val sg = sign_of thy;
     val frees = map dest_Free (term_frees t);
+    val szname = variant (map fst frees) "i";
     val s = "structure TestTerm =\nstruct\n\n" ^
       setmp mode ["term_of", "test"] (generate_code_i thy)
         [("testf", list_abs_free (frees, t))] ^
       "\n" ^ Pretty.string_of
         (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
-          Pretty.brk 1, Pretty.str "(fn i =>", Pretty.brk 1,
+          Pretty.brk 1, Pretty.str ("(fn " ^ szname ^ " =>"), Pretty.brk 1,
           Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
             Pretty.blk (0, separate Pretty.fbrk (map (fn (s, T) =>
               Pretty.block [Pretty.str ("val " ^ s ^ " ="), Pretty.brk 1,
               mk_gen sg false [] "" T, Pretty.brk 1,
-              Pretty.str "i;"]) frees)),
+              Pretty.str (szname ^ ";")]) frees)),
             Pretty.brk 1, Pretty.str "in", Pretty.brk 1,
             Pretty.block [Pretty.str "if ",
               mk_app false (Pretty.str "testf") (map (Pretty.str o fst) frees),