--- 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"