1.1 --- a/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:32 2014 +0200
     1.2 +++ b/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:33 2014 +0200
     1.3 @@ -8,6 +8,11 @@
     1.4  imports Lifting Basic_BNFs
     1.5  begin
     1.6  
     1.7 +(* The following lemma can be deleted when product is added to FP sugar *)
     1.8 +lemma prod_pred_inject [simp]:
     1.9 +  "pred_prod P1 P2 (a, b) = (P1 a \<and> P2 b)"
    1.10 +  unfolding pred_prod_def fun_eq_iff prod_set_simps by blast
    1.11 +
    1.12  subsection {* Transfer rules for the Transfer package *}
    1.13  
    1.14  context