# HG changeset patch
# User wenzelm
# Date 1457284509 -3600
# Node ID 5499461a0203ae8bc551591d197c366a387b61f2
# Parent  8b7bdfc09f3bd27fe32b889f9f5456dcb0791229
avoid redundant escapes;

diff -r 8b7bdfc09f3b -r 5499461a0203 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- 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