# HG changeset patch
# User berghofe
# Date 1101289058 -3600
# Node ID ff21cddee4427d7724d0a904711d2b31ad0d3a4f
# Parent  50ac7d2c34c9c09313c6d9af6838ea170ca41951
Made test_term escape special characters in strings that caused the
ML compiler to fail.

diff -r 50ac7d2c34c9 -r ff21cddee442 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Nov 24 10:32:33 2004 +0100
+++ b/src/Pure/codegen.ML	Wed Nov 24 10:37:38 2004 +0100
@@ -642,7 +642,7 @@
               Pretty.block [Pretty.str "Library.Some ", Pretty.block (Pretty.str "[" ::
                 flat (separate [Pretty.str ",", Pretty.brk 1]
                   (map (fn (s, T) => [Pretty.block
-                    [Pretty.str ("(" ^ Library.quote s ^ ","), Pretty.brk 1,
+                    [Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1,
                      mk_app false (mk_term_of sg false T)
                        [Pretty.str (mk_id s)], Pretty.str ")"]]) frees)) @
                   [Pretty.str "]"])]],