src/HOL/Tools/Quickcheck/narrowing_generators.ML

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Mar 01 21:00:38 2016 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Mar 01 21:10:29 2016 +0100
@@ -206,7 +206,7 @@
 
 fun exec verbose code =
   ML_Context.exec (fn () =>
-    Secure.use_text ML_Env.local_context
+    use_text ML_Env.local_context
       {line = 0, file = "generated code", verbose = verbose, debug = false} code)
 
 fun with_overlord_dir name f =