# HG changeset patch
# User bulwahn
# Date 1302273074 -7200
# Node ID 12635bb655fd0c2da33e189b5f65d9b267743285
# Parent  95dfa082065a170fe444693be163dca7efa09810
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments

diff -r 95dfa082065a -r 12635bb655fd src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Fri Apr 08 16:31:14 2011 +0200
+++ b/src/HOL/Library/Code_Char.thy	Fri Apr 08 16:31:14 2011 +0200
@@ -59,6 +59,6 @@
   (Scala "!(_.toList)")
 
 
-declare Quickcheck_Exhaustive.char.bounded_forall_char.simps [code del]
+(*declare Quickcheck_Exhaustive.char.bounded_forall_char.simps [code del]*)
 
 end
diff -r 95dfa082065a -r 12635bb655fd src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
@@ -533,13 +533,13 @@
 
 val setup =
   Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+      (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype))
+(* #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
   #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
-      (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype))
-  #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{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))
+      (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
   #> setup_smart_quantifier
   #> setup_full_support
   #> setup_fast