# HG changeset patch
# User wenzelm
# Date 1330341148 -3600
# Node ID 879f5c76ffb61829b2984303aedb82f183720e5d
# Parent  1fef02b93723b65720146d4303246994979beea0
reactivated Find_Unused_Assms_Examples to avoid untested / dead stuff in the repository;
moved the whole HOL-Quickcheck_Examples target from "all" to "full" for now -- it does not terminate in certain situations (to be investigated further);

diff -r 1fef02b93723 -r 879f5c76ffb6 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Feb 27 11:53:08 2012 +0100
+++ b/src/HOL/IsaMakefile	Mon Feb 27 12:12:28 2012 +0100
@@ -61,7 +61,6 @@
   HOL-Nitpick_Examples \
   HOL-Number_Theory \
   HOL-Old_Number_Theory \
-  HOL-Quickcheck_Examples \
   HOL-Quotient_Examples \
   HOL-Predicate_Compile_Examples \
   HOL-Prolog \
@@ -96,7 +95,7 @@
   HOL-Nominal-Examples
 
 all: test-no-smlnj test images-no-smlnj images
-full: all benchmark
+full: all benchmark HOL-Quickcheck_Examples
 smlnj: test images
 
 
diff -r 1fef02b93723 -r 879f5c76ffb6 src/HOL/Quickcheck_Examples/ROOT.ML
--- a/src/HOL/Quickcheck_Examples/ROOT.ML	Mon Feb 27 11:53:08 2012 +0100
+++ b/src/HOL/Quickcheck_Examples/ROOT.ML	Mon Feb 27 12:12:28 2012 +0100
@@ -1,4 +1,5 @@
 use_thys [
+  "Find_Unused_Assms_Examples",
   "Quickcheck_Examples",
   "Quickcheck_Lattice_Examples"
 ];