diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Lifting_Set.thy --- a/src/HOL/Lifting_Set.thy Mon Oct 17 14:37:32 2016 +0200 +++ b/src/HOL/Lifting_Set.thy Mon Oct 17 17:33:07 2016 +0200 @@ -286,7 +286,7 @@ qed lemmas sum_parametric = sum.F_parametric -lemmas setprod_parametric = setprod.F_parametric +lemmas prod_parametric = prod.F_parametric lemma rel_set_UNION: assumes [transfer_rule]: "rel_set Q A B" "rel_fun Q (rel_set R) f g"