--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun Mar 06 16:19:02 2016 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun Mar 06 18:15:09 2016 +0100
@@ -279,7 +279,6 @@
let
val output_value = the_default "NONE"
(try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
- |> 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