--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Aug 17 15:29:30 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Aug 17 16:27:12 2015 +0200
@@ -205,7 +205,9 @@
File.read @{path "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
fun exec verbose code =
- ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
+ ML_Context.exec (fn () =>
+ Secure.use_text ML_Env.local_context
+ {line = 0, file = "generated code", verbose = verbose, debug = false} code)
fun with_overlord_dir name f =
let