src/HOL/Tools/Quickcheck/random_generators.ML
changeset 43875 485d2ad43528
parent 43333 2bdec7f430d3
child 43876 b8fa7287ee4c
     1.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sun Jul 17 22:25:14 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jul 18 10:34:21 2011 +0200
     1.3 @@ -438,14 +438,15 @@
     1.4        end
     1.5    end;
     1.6  
     1.7 -
     1.8 +val test_goals = Quickcheck.generator_test_goal_terms;
     1.9 +  
    1.10  (** setup **)
    1.11  
    1.12  val setup =
    1.13    Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    1.14      (((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype))
    1.15    #> Code_Target.extend_target (target, (Code_Runtime.target, K I))
    1.16 -  #> Context.theory_map
    1.17 -    (Quickcheck.add_generator ("random", compile_generator_expr));
    1.18 +  #> Context.theory_map (Quickcheck.add_generator ("random", compile_generator_expr))
    1.19 +  #> Context.theory_map (Quickcheck.add_tester ("random", test_goals));
    1.20  
    1.21  end;