1.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Nov 30 09:21:04 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Nov 30 09:21:07 2011 +0100
     1.3 @@ -287,14 +287,14 @@
     1.4  fun mk_test_term lookup mk_closure mk_if none_t return ctxt =
     1.5    let
     1.6      fun mk_naive_test_term t =
     1.7 -      fold_rev mk_closure (map lookup (Term.add_free_names t [])) (mk_if (t, none_t, return)) 
     1.8 +      fold_rev mk_closure (map lookup (Term.add_free_names t [])) (mk_if (t, none_t, return))
     1.9      fun mk_smart_test_term' concl bound_vars assms =
    1.10        let
    1.11          fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
    1.12          val (vars, check) =
    1.13            case assms of [] => (vars_of concl, (concl, none_t, return))
    1.14 -            | assm :: assms => (vars_of assm, (assm,
    1.15 -                mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t))
    1.16 +            | assm :: assms => (vars_of assm, (HOLogic.mk_not assm, none_t, 
    1.17 +                mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms))
    1.18        in
    1.19          fold_rev mk_closure (map lookup vars) (mk_if check)
    1.20        end
    1.21 @@ -375,9 +375,10 @@
    1.22              $ lambda free (lambda term_var t)) $ depth
    1.23      val none_t = @{term "None :: term list option"}
    1.24      fun mk_safe_if (cond, then_t, else_t) =
    1.25 -      @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
    1.26 -        (@{term "If :: bool => term list option => term list option => term list option"}
    1.27 -        $ cond $ then_t $ else_t) $ none_t;
    1.28 +      @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"}
    1.29 +        $ (@{term "If :: bool => term list option => term list option => term list option"}
    1.30 +        $ cond $ then_t $ else_t)
    1.31 +        $ (if Config.get ctxt Quickcheck.potential then else_t else none_t);
    1.32      val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_safe_if none_t return ctxt
    1.33    in lambda depth (mk_test_term t) end
    1.34