# HG changeset patch
# User bulwahn
# Date 1307603233 -7200
# Node ID f9283eb3a4bf81e72edb25b774970b1b257021ba
# Parent  3e274608f06b3043e20891dc1458a225d589baf6
fixing code generation test

diff -r 3e274608f06b -r f9283eb3a4bf src/HOL/Codegenerator_Test/Generate_Pretty.thy
--- 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 {*
diff -r 3e274608f06b -r f9283eb3a4bf src/HOL/Quickcheck_Narrowing.thy
--- 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"
diff -r 3e274608f06b -r f9283eb3a4bf src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- 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