# HG changeset patch
# User bulwahn
# Date 1310989715 -7200
# Node ID 4690f76f327a4d5e32871702beb3b0cb39520594
# Parent  eba9c3b1f84a76050f8e7c3fd49bbdbc9544ad20
making active configuration public in narrowing-based quickcheck

diff -r eba9c3b1f84a -r 4690f76f327a src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 18 11:38:14 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 18 13:48:35 2011 +0200
@@ -9,6 +9,7 @@
   val allow_existentials : bool Config.T
   val finite_functions : bool Config.T
   val overlord : bool Config.T
+  val active : bool Config.T
   val test_term: Proof.context -> bool * bool -> term * term list -> Quickcheck.result
   datatype counterexample = Universal_Counterexample of (term * counterexample)
     | Existential_Counterexample of (term * counterexample) list