# HG changeset patch
# User bulwahn
# Date 1308033018 -7200
# Node ID d7ae1fae113b27ee10c13e30ec89323d4273ec94
# Parent  ba199d75bc7e96ed5fd1c291909b6cbf4158e82f
removed comment and declaration after issue has been resolved (cf. e83695ea0e0a)

diff -r ba199d75bc7e -r d7ae1fae113b src/HOL/Quickcheck_Narrowing.thy
--- 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"