diff -r 9084d77f1119 -r bcf2123d059a src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Aug 23 15:19:32 2016 +0200
+++ b/src/HOL/List.thy	Wed Aug 24 11:02:23 2016 +0200
@@ -2766,6 +2766,10 @@
 
 subsubsection \<open>@{const List.product} and @{const product_lists}\<close>
 
+lemma product_concat_map:
+  "List.product xs ys = concat (map (\<lambda>x. map (\<lambda>y. (x,y)) ys) xs)"
+by(induction xs) (simp)+
+
 lemma set_product[simp]: "set (List.product xs ys) = set xs \<times> set ys"
 by (induct xs) auto