# HG changeset patch
# User haftmann
# Date 1482520347 -3600
# Node ID f77b946d18aa6c72bef0724b1a3b722fc47d31e5
# Parent  ce441970956fe94ce67064763541d83bed688412
restored instance for char, which got ancidentally lost in b3f2b8c906a6

diff -r ce441970956f -r f77b946d18aa src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Dec 23 20:10:38 2016 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Dec 23 20:12:27 2016 +0100
@@ -476,13 +476,18 @@
 
 end
 
-(* FIXME instantiation char :: check_all
+instantiation char :: check_all
 begin
 
-definition
-  "check_all f = check_all (\<lambda>(x, t1). check_all (\<lambda>(y, t2).
-     f (Char x y, \<lambda>_. Code_Evaluation.App
-       (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
+primrec check_all_char' ::
+  "(char \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> char list \<Rightarrow> (bool \<times> term list) option"
+  where "check_all_char' f [] = None"
+  | "check_all_char' f (c # cs) = f (c, \<lambda>_. Code_Evaluation.term_of c)
+      orelse check_all_char' f cs"
+
+definition check_all_char ::
+  "(char \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> (bool \<times> term list) option"
+  where "check_all f = check_all_char' f Enum.enum"
 
 definition enum_term_of_char :: "char itself \<Rightarrow> unit \<Rightarrow> term list"
 where
@@ -490,7 +495,7 @@
 
 instance ..
 
-end *)
+end
 
 instantiation option :: (check_all) check_all
 begin