--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Tue Oct 13 09:21:15 2015 +0200
@@ -338,7 +338,7 @@
"jad = apsnd transpose o length_permutate o map sparsify"
definition
- "jad_mv v = inflate o split zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
+ "jad_mv v = inflate o case_prod zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
lemma "matrix (M::int list list) rs cs \<Longrightarrow> False"
quickcheck[tester = smart_exhaustive, size = 6]