
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 [[]]) [(\<lambda>_. a)])"




