--- a/src/HOL/Quickcheck_Narrowing.thy Mon Jun 13 23:21:53 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Tue Jun 14 08:30:18 2011 +0200
@@ -207,14 +207,6 @@
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"