renewed prolog-quickcheck
authorbulwahn
Thu Nov 10 17:28:02 2011 +0100 (2011-11-10)
changeset 454422b91e27676b2
parent 45441 fb4ac1dd4fde
child 45443 c8a9a5e577bd
renewed prolog-quickcheck
src/HOL/Tools/Predicate_Compile/code_prolog.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Nov 10 17:26:17 2011 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Nov 10 17:28:02 2011 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4    
     1.5    val active : bool Config.T
     1.6    val test_goals :
     1.7 -    Proof.context -> (bool * bool) -> (string * typ) list -> (term * term list) list ->
     1.8 +    Proof.context -> bool -> (string * typ) list -> (term * term list) list ->
     1.9        Quickcheck.result list
    1.10  
    1.11    val trace : bool Unsynchronized.ref
    1.12 @@ -1015,7 +1015,7 @@
    1.13  
    1.14  val active = Attrib.setup_config_bool @{binding quickcheck_prolog_active} (K true);
    1.15  
    1.16 -fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
    1.17 +fun test_term ctxt (t, eval_terms) =
    1.18    let
    1.19      val t' = fold_rev absfree (Term.add_frees t []) t
    1.20      val options = code_options_of (Proof_Context.theory_of ctxt)
    1.21 @@ -1043,11 +1043,11 @@
    1.22         evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []}
    1.23    end;
    1.24  
    1.25 -fun test_goals ctxt (limit_time, is_interactive) insts goals =
    1.26 +fun test_goals ctxt _ insts goals =
    1.27    let
    1.28      val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
    1.29    in
    1.30 -    Quickcheck_Common.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
    1.31 +    Quickcheck_Common.collect_results (test_term ctxt) (maps (map snd) correct_inst_goals) []
    1.32    end
    1.33    
    1.34