diff -r 5a0c06491974 -r 507c90523113 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -280,7 +280,7 @@
                   val output_value = the_default "NONE"
                     (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
                   val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
-                    ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
+                    ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))";
                   val ctxt' = ctxt
                     |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
                     |> Context.proof_map (exec false ml_code);