# HG changeset patch
# User berghofe
# Date 1086715357 -7200
# Node ID b792081d2399c4607febec1658fba3d8a0bae70a
# Parent  0a840138dcd7c7d31f2843286db5170c9972f105
mk_id is now also applied to identifiers in test_term.

diff -r 0a840138dcd7 -r b792081d2399 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue Jun 08 16:40:41 2004 +0200
+++ b/src/Pure/codegen.ML	Tue Jun 08 19:22:37 2004 +0200
@@ -586,12 +586,12 @@
           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,
+              Pretty.block [Pretty.str ("val " ^ mk_id s ^ " ="), Pretty.brk 1,
               mk_gen sg false [] "" T, Pretty.brk 1,
               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),
+              mk_app false (Pretty.str "testf") (map (Pretty.str o mk_id o fst) frees),
               Pretty.brk 1, Pretty.str "then Library.None",
               Pretty.brk 1, Pretty.str "else ",
               Pretty.block [Pretty.str "Library.Some ", Pretty.block (Pretty.str "[" ::
@@ -599,7 +599,7 @@
                   (map (fn (s, T) => [Pretty.block
                     [Pretty.str ("(" ^ Library.quote s ^ ","), Pretty.brk 1,
                      mk_app false (mk_term_of sg false T)
-                       [Pretty.str s], Pretty.str ")"]]) frees)) @
+                       [Pretty.str (mk_id s)], Pretty.str ")"]]) frees)) @
                   [Pretty.str "]"])]],
             Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"])) ^
       "\n\nend;\n";