src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42020 2da02764d523
parent 42019 a9445d87bc3e
child 42023 1bd4b6d1c482
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
@@ -147,6 +147,7 @@
     val result = Isabelle_System.with_tmp_dir tmp_prefix run
     val output_value = the_default "NONE"
       (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result)
+      |> translate_string (fn s => if s = "\\" then "\\\\" else s)
     val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
       ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
     val ctxt' = ctxt