--- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy Thu Jun 09 08:32:22 2011 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy Thu Jun 09 09:07:13 2011 +0200
@@ -10,6 +10,10 @@
lemma [code, code del]: "nat_of_char = nat_of_char" ..
lemma [code, code del]: "char_of_nat = char_of_nat" ..
+declare Quickcheck_Narrowing.zero_code_int_code[code del]
+declare Quickcheck_Narrowing.one_code_int_code[code del]
+declare Quickcheck_Narrowing.int_of_code[code del]
+
subsection {* Check whether generated code compiles *}
text {*
--- a/src/HOL/Quickcheck_Narrowing.thy Thu Jun 09 08:32:22 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Thu Jun 09 09:07:13 2011 +0200
@@ -207,6 +207,13 @@
subsubsection {* Narrowing's deep representation of types and terms *}
datatype narrowing_type = SumOfProd "narrowing_type list list"
+text {*
+The definition of the automatically derived equal type class instance for @{typ narrowing_type}
+causes an error in the OCaml serializer.
+For the moment, we delete this equation manually because we do not require an executable equality
+on this type anyway.
+*}
+declare Quickcheck_Narrowing.equal_narrowing_type_def[code del]
datatype narrowing_term = Var "code_int list" narrowing_type | Ctr code_int "narrowing_term list"
datatype 'a cons = C narrowing_type "(narrowing_term list => 'a) list"
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jun 09 08:32:22 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jun 09 09:07:13 2011 +0200
@@ -358,8 +358,8 @@
end
fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
- fst (Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
- (t, mk_case_term ctxt (p - 1) qs' c)) cs))
+ Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
+ (t, mk_case_term ctxt (p - 1) qs' c)) cs)
| mk_case_term ctxt p ((@{const_name All}, (x, T)) :: qs') (Universal_Counterexample (t, c)) =
if p = 0 then t else mk_case_term ctxt (p - 1) qs' c