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