Made test_term escape special characters in strings that caused the
authorberghofe
Wed Nov 24 10:37:38 2004 +0100 (2004-11-24)
changeset 15326ff21cddee442
parent 15325 50ac7d2c34c9
child 15327 0230a10582d3
Made test_term escape special characters in strings that caused the
ML compiler to fail.
src/Pure/codegen.ML
     1.1 --- a/src/Pure/codegen.ML	Wed Nov 24 10:32:33 2004 +0100
     1.2 +++ b/src/Pure/codegen.ML	Wed Nov 24 10:37:38 2004 +0100
     1.3 @@ -642,7 +642,7 @@
     1.4                Pretty.block [Pretty.str "Library.Some ", Pretty.block (Pretty.str "[" ::
     1.5                  flat (separate [Pretty.str ",", Pretty.brk 1]
     1.6                    (map (fn (s, T) => [Pretty.block
     1.7 -                    [Pretty.str ("(" ^ Library.quote s ^ ","), Pretty.brk 1,
     1.8 +                    [Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1,
     1.9                       mk_app false (mk_term_of sg false T)
    1.10                         [Pretty.str (mk_id s)], Pretty.str ")"]]) frees)) @
    1.11                    [Pretty.str "]"])]],