# HG changeset patch
# User blanchet
# Date 1409695577 -7200
# Node ID 3cfbb68ad2e07f6556b4def093570a6dd241e765
# Parent  00c878bd20934a8a6af8fd70e6ac20797aca3c76
ported Quickcheck to support new datatypes better

diff -r 00c878bd2093 -r 3cfbb68ad2e0 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Sep 02 23:59:49 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Sep 03 00:06:17 2014 +0200
@@ -254,7 +254,7 @@
   let
     val cnstrs = flat (maps
       (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
-      (Symtab.dest (Old_Datatype_Data.get_all (Proof_Context.theory_of ctxt))))
+      (Symtab.dest (BNF_LFP_Compat.get_all (Proof_Context.theory_of ctxt) BNF_LFP_Compat.Keep_Nesting)))
     fun is_constrt (Const (s, T), ts) = (case (AList.lookup (op =) cnstrs s, body_type T) of
         (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname'
       | _ => false)
@@ -537,20 +537,14 @@
   Quickcheck_Common.datatype_interpretation (@{sort exhaustive}, instantiate_exhaustive_datatype)
 
 val setup_bounded_forall_datatype_interpretation =
-  Old_Datatype_Data.interpretation (Quickcheck_Common.ensure_sort
+  BNF_LFP_Compat.interpretation BNF_LFP_Compat.Keep_Nesting (Quickcheck_Common.ensure_sort
     (((@{sort type}, @{sort type}), @{sort bounded_forall}),
-    (Old_Datatype_Data.the_descr, instantiate_bounded_forall_datatype)))
+    (fn thy => BNF_LFP_Compat.the_descr thy BNF_LFP_Compat.Keep_Nesting, instantiate_bounded_forall_datatype)))
 
 val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
 
 val setup =
   Quickcheck_Common.datatype_interpretation (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
-(* #> Old_Datatype_Data.interpretation (Quickcheck_Common.ensure_sort_datatype
-      (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
-  #> Old_Datatype_Data.interpretation (Quickcheck_Common.ensure_sort_datatype
-      (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
-  #> Old_Datatype_Data.interpretation (Quickcheck_Common.ensure_sort_datatype
-      (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
   #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, 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 00c878bd2093 -r 3cfbb68ad2e0 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Sep 02 23:59:49 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Sep 03 00:06:17 2014 +0200
@@ -419,9 +419,11 @@
   end;
 
 fun ensure_common_sort_datatype (sort, instantiate) =
-  ensure_sort (((@{sort typerep}, @{sort term_of}), sort), (Old_Datatype_Data.the_descr, instantiate))
+  ensure_sort (((@{sort typerep}, @{sort term_of}), sort),
+    (fn thy => BNF_LFP_Compat.the_descr thy BNF_LFP_Compat.Keep_Nesting, instantiate))
 
-val datatype_interpretation = Old_Datatype_Data.interpretation o ensure_common_sort_datatype
+val datatype_interpretation =
+  BNF_LFP_Compat.interpretation BNF_LFP_Compat.Keep_Nesting o ensure_common_sort_datatype
   
 (** generic parametric compilation **)