# HG changeset patch
# User bulwahn
# Date 1322774075 -3600
# Node ID 8d8c926bcffe220a21b0aa4a2e076637a55d2772
# Parent  6bd0acefaedbdd871d10c89ede7d4f1111fca9a1
adapting exhaustive generators in record package

diff -r 6bd0acefaedb -r 8d8c926bcffe src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/record.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -1798,11 +1798,11 @@
     val size = @{term "i::code_numeral"};
     fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
     val T = Type (tyco, map TFree vs);
-    val test_function = Free ("f", termifyT T --> @{typ "term list option"});
+    val test_function = Free ("f", termifyT T --> @{typ "(bool * term list) option"});
     val params = Name.invent_names Name.context "x" Ts;
     fun full_exhaustiveT T =
-      (termifyT T --> @{typ "Code_Evaluation.term list option"}) -->
-        @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"};
+      (termifyT T --> @{typ "(bool * Code_Evaluation.term list) option"}) -->
+        @{typ code_numeral} --> @{typ "(bool * Code_Evaluation.term list) option"};
     fun mk_full_exhaustive T =
       Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
         full_exhaustiveT T);