diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/Permutations.thy Tue Oct 13 09:21:15 2015 +0200
@@ -196,7 +196,7 @@
by (auto intro: card_ge_0_finite)
then have pF'f: "finite ?pF'"
using H0 \finite F\
- apply (simp only: Collect_split Collect_mem_eq)
+ apply (simp only: Collect_case_prod Collect_mem_eq)
apply (rule finite_cartesian_product)
apply simp_all
done
@@ -246,7 +246,7 @@
from pFs H0 have xFc: "card ?xF = fact n"
unfolding xfgpF' card_image[OF ginj]
using \finite F\ \finite ?pF\
- apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
+ apply (simp only: Collect_case_prod Collect_mem_eq card_cartesian_product)
apply simp
done
from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF"