# HG changeset patch
# User bulwahn
# Date 1310978061 -7200
# Node ID abd1f074cb986602f140068fe8e93b5e45fcddcd
# Parent  b8fa7287ee4ca2797312602a06da2a19b40816a9
removing generator registration

diff -r b8fa7287ee4c -r abd1f074cb98 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Jul 18 10:34:21 2011 +0200
@@ -501,7 +501,6 @@
       (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
   #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
-  #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
   #> Context.theory_map (Quickcheck.add_tester ("exhaustive", test_goals))
   #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
   #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));
diff -r b8fa7287ee4c -r abd1f074cb98 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jul 18 10:34:21 2011 +0200
@@ -446,7 +446,6 @@
   Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
     (((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype))
   #> Code_Target.extend_target (target, (Code_Runtime.target, K I))
-  #> Context.theory_map (Quickcheck.add_generator ("random", compile_generator_expr))
   #> Context.theory_map (Quickcheck.add_tester ("random", test_goals));
 
 end;
diff -r b8fa7287ee4c -r abd1f074cb98 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon Jul 18 10:34:21 2011 +0200
@@ -924,7 +924,9 @@
   | test_term ctxt _ =
       error "Compilation of multiple instances is not supported by tester SML_inductive";
 
+val test_goal = Quickcheck.generator_test_goal_terms test_term;
+
 val quickcheck_setup =
-  Context.theory_map (Quickcheck.add_generator ("SML_inductive", test_term));
+  Context.theory_map (Quickcheck.add_tester ("SML_inductive", test_goal));
 
 end;
diff -r b8fa7287ee4c -r abd1f074cb98 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/Tools/quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
@@ -43,9 +43,9 @@
   val counterexample_of : result -> (string * term) list option
   val timings_of : result -> (string * int) list
   (* registering generators *)
-  val add_generator:
+  (*val add_generator:
     string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)
-      -> Context.generic -> Context.generic
+      -> Context.generic -> Context.generic*)
   val add_tester:
     string * (Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list)
       -> Context.generic -> Context.generic
@@ -196,17 +196,16 @@
 structure Data = Generic_Data
 (
   type T =
-    (((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list
-      * (string * (Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list)) list)
+    ((string * (Proof.context -> bool * bool ->
+      (string * typ) list -> (term * term list) list -> result list)) list
       * ((string * (Proof.context -> term list -> (int -> term list option) list)) list
       * ((string * (Proof.context -> term list -> (int -> bool) list)) list)))
       * test_params;
-  val empty = ((([], []), ([], [])), Test_Params {default_type = [], expect = No_Expectation});
+  val empty = (([], ([], [])), Test_Params {default_type = [], expect = No_Expectation});
   val extend = I;
-  fun merge ((((generators1, testers1), (batch_generators1, batch_validators1)), params1),
-    (((generators2, testers2), (batch_generators2, batch_validators2)), params2)) : T =
-    (((AList.merge (op =) (K true) (generators1, generators2),
-       AList.merge (op =) (K true) (testers1, testers2)),
+  fun merge (((testers1, (batch_generators1, batch_validators1)), params1),
+    ((testers2, (batch_generators2, batch_validators2)), params2)) : T =
+    ((AList.merge (op =) (K true) (testers1, testers2),
       (AList.merge (op =) (K true) (batch_generators1, batch_generators2),
        AList.merge (op =) (K true) (batch_validators1, batch_validators2))),
       merge_test_params (params1, params2));
@@ -220,9 +219,9 @@
 
 val map_test_params = Data.map o apsnd o map_test_params'
 
-val add_generator = Data.map o apfst o apfst o apfst o AList.update (op =);
+(*val add_generator = Data.map o apfst o apfst o apfst o AList.update (op =);*)
 
-val add_tester = Data.map o apfst o apfst o apsnd o AList.update (op =);
+val add_tester = Data.map o apfst o apfst o AList.update (op =);
 
 val add_batch_generator = Data.map o apfst o apsnd o apfst o AList.update (op =);
 
@@ -255,9 +254,8 @@
   gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o snd o fst o Data.get o Context.Proof) ctxt))
 val mk_batch_validator =
   gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o snd o fst o Data.get o Context.Proof) ctxt))
-
   
-fun lookup_tester ctxt = AList.lookup (op =) ((snd o fst o fst o Data.get o Context.Proof) ctxt)
+fun lookup_tester ctxt = AList.lookup (op =) ((fst o fst o Data.get o Context.Proof) ctxt)
 
 (* testing propositions *)
 
@@ -578,10 +576,8 @@
   | read_expectation "counterexample" = Counterexample
   | read_expectation s = error ("Not an expectation value: " ^ s)
 
-fun valid_tester_name genctxt name =
-  AList.defined (op =) (fst (fst (fst (Data.get genctxt)))) name orelse
-    AList.defined (op =) (snd (fst (fst (Data.get genctxt)))) name
-
+fun valid_tester_name genctxt name = AList.defined (op =) (fst (fst (Data.get genctxt))) name
+  
 fun parse_tester name genctxt =
   if valid_tester_name genctxt name then
     Config.put_generic tester name genctxt