diff r 5407bc278c9a r b11b7ad22684 src/HOL/Quickcheck_Narrowing.thy
 a/src/HOL/Quickcheck_Narrowing.thy Thu Apr 13 10:10:06 2017 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Thu Apr 13 10:10:08 2017 +0200
@@ 84,10 +84,6 @@
type_synonym 'a narrowing = "integer => 'a narrowing_cons"
definition empty :: "'a narrowing"
where
 "empty d = Narrowing_cons (Narrowing_sum_of_products []) []"

definition cons :: "'a => 'a narrowing"
where
"cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(\_. a)])"