diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -379,42 +379,13 @@
 
 end
 
-instantiation nibble :: check_all
+(* FIXME instantiation char :: check_all
 begin
 
 definition
-  "check_all f =
-    f (Code_Evaluation.valtermify Nibble0) orelse
-    f (Code_Evaluation.valtermify Nibble1) orelse
-    f (Code_Evaluation.valtermify Nibble2) orelse
-    f (Code_Evaluation.valtermify Nibble3) orelse
-    f (Code_Evaluation.valtermify Nibble4) orelse
-    f (Code_Evaluation.valtermify Nibble5) orelse
-    f (Code_Evaluation.valtermify Nibble6) orelse
-    f (Code_Evaluation.valtermify Nibble7) orelse
-    f (Code_Evaluation.valtermify Nibble8) orelse
-    f (Code_Evaluation.valtermify Nibble9) orelse
-    f (Code_Evaluation.valtermify NibbleA) orelse
-    f (Code_Evaluation.valtermify NibbleB) orelse
-    f (Code_Evaluation.valtermify NibbleC) orelse
-    f (Code_Evaluation.valtermify NibbleD) orelse
-    f (Code_Evaluation.valtermify NibbleE) orelse
-    f (Code_Evaluation.valtermify NibbleF)"
-
-definition enum_term_of_nibble :: "nibble itself => unit => term list"
-where
-  "enum_term_of_nibble = (%_ _. map Code_Evaluation.term_of (Enum.enum :: nibble list))"
-
-instance ..
-
-end
-
-
-instantiation char :: check_all
-begin
-
-definition
-  "check_all f = check_all (%(x, t1). check_all (%(y, t2). f (Char x y, %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
+  "check_all f = check_all (%(x, t1). check_all (%(y, t2).
+     f (Char x y, %_. Code_Evaluation.App
+       (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
 
 definition enum_term_of_char :: "char itself => unit => term list"
 where
@@ -422,8 +393,7 @@
 
 instance ..
 
-end
-
+end *)
 
 instantiation option :: (check_all) check_all
 begin
@@ -624,13 +594,7 @@
 
 ML_file "Tools/Quickcheck/abstract_generators.ML"
 
-lemma check_all_char [code]:
-  "check_all f = check_all (\<lambda>(x, t1). check_all (\<lambda>(y, t2).
-     f (char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y), \<lambda>_. Code_Evaluation.App (Code_Evaluation.App
-       (Code_Evaluation.term_of (\<lambda>x y. char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y))) (t1 ())) (t2 ()))))"
-  by (simp add: check_all_char_def)
-
-instantiation char :: full_exhaustive
+(* FIXME instantiation char :: full_exhaustive
 begin
 
 definition full_exhaustive_char
@@ -648,7 +612,7 @@
 
 instance ..
 
-end
+end *)
 
 hide_fact (open) orelse_def
 no_notation orelse (infixr "orelse" 55)