--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Apr 08 19:39:08 2015 +0200
@@ -236,7 +236,7 @@
val rewrs = map (swap o dest) @{thms all_simps} @
(map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff},
@{thm bot_fun_def}, @{thm less_bool_def}])
- val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term thy t)
+ val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term ctxt t)
val (vs, body) = strip_all t'
val vs' = Variable.variant_frees ctxt [t'] vs
in