src/HOL/Quickcheck_Narrowing.thy
changeset 65482 721feefce9c6
parent 65481 b11b7ad22684
child 66148 5e60c2d0a1f1
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Apr 13 10:10:08 2017 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Apr 13 10:10:09 2017 +0200
@@ -99,13 +99,14 @@
 
 definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing"
 where
-  "apply f a d =
+  "apply f a d = (if d > 0 then
      (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs \<Rightarrow>
        case a (d - 1) of Narrowing_cons ta cas \<Rightarrow>
        let
-         shallow = d > 0 \<and> non_empty ta;
+         shallow = non_empty ta;
          cs = [(\<lambda>(x # xs) \<Rightarrow> cf xs (conv cas x)). shallow, cf \<leftarrow> cfs]
-       in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p \<leftarrow> ps]) cs)"
+       in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p \<leftarrow> ps]) cs)
+     else Narrowing_cons (Narrowing_sum_of_products []) [])"
 
 definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
 where