1.1 --- a/src/Tools/quickcheck.ML	Thu Jun 02 08:55:08 2011 +0200
     1.2 +++ b/src/Tools/quickcheck.ML	Thu Jun 02 09:51:40 2011 +0200
     1.3 @@ -457,18 +457,21 @@
     1.4          collect_results f ts (result :: results)
     1.5      end  
     1.6  
     1.7 -fun test_goal_terms lthy (limit_time, is_interactive) insts goals =
     1.8 +fun test_goal_terms ctxt (limit_time, is_interactive) insts goals =
     1.9    let
    1.10      fun test_term' goal =
    1.11        case goal of
    1.12 -        [(NONE, t)] => test_term lthy (limit_time, is_interactive) t
    1.13 -      | ts => test_term_with_increasing_cardinality lthy (limit_time, is_interactive) (map snd ts)
    1.14 -    val correct_inst_goals = instantiate_goals lthy insts goals
    1.15 +        [(NONE, t)] => test_term ctxt (limit_time, is_interactive) t
    1.16 +      | ts => test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) (map snd ts)
    1.17 +    val correct_inst_goals = instantiate_goals ctxt insts goals
    1.18    in
    1.19 -    if Config.get lthy finite_types then
    1.20 -      collect_results test_term' correct_inst_goals []
    1.21 -    else
    1.22 -      collect_results (test_term lthy (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
    1.23 +    case lookup_tester ctxt (Config.get ctxt tester) of
    1.24 +      SOME test_goal_terms => test_goal_terms ctxt (limit_time, is_interactive) insts goals
    1.25 +    | NONE =>
    1.26 +        if Config.get ctxt finite_types then
    1.27 +          collect_results test_term' correct_inst_goals []
    1.28 +        else
    1.29 +          collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
    1.30    end;
    1.31  
    1.32  fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state =
    1.33 @@ -492,9 +495,8 @@
    1.34        | SOME locale =>
    1.35          map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
    1.36            (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
    1.37 -    val test_goals = the_default test_goal_terms (lookup_tester lthy (Config.get lthy tester))
    1.38    in
    1.39 -    test_goals lthy (time_limit, is_interactive) insts goals
    1.40 +    test_goal_terms lthy (time_limit, is_interactive) insts goals
    1.41    end
    1.42  
    1.43  (* pretty printing *)