src/HOL/Tools/smallvalue_generators.ML
changeset 40644 0850a2a16dce
parent 40641 5615cc557120
child 40840 2f97215e79bf
--- a/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:42:06 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:42:07 2010 +0100
@@ -206,7 +206,7 @@
   let
     val Ts = (map snd o fst o strip_abs) t;
     val thy = ProofContext.theory_of ctxt
-  in if Quickcheck.report ctxt then
+  in if Config.get ctxt Quickcheck.report then
     error "Compilation with reporting facility is not supported"
   else
     let