removed comment and declaration after issue has been resolved (cf. e83695ea0e0a)
authorbulwahn
Tue, 14 Jun 2011 08:30:18 +0200
changeset 43378 d7ae1fae113b
parent 43377 ba199d75bc7e
child 43379 8c4b383e5143
removed comment and declaration after issue has been resolved (cf. e83695ea0e0a)
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"