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