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