add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons

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

--- a/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:32 2014 +0200
+++ b/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:33 2014 +0200
@@ -8,6 +8,11 @@
 imports Lifting Basic_BNFs
 begin
 
+(* The following lemma can be deleted when sum is added to FP sugar *)
+lemma sum_pred_inject [simp]:
+  "pred_sum P1 P2 (Inl a) = P1 a" and "pred_sum P1 P2 (Inr a) = P2 a"
+  unfolding pred_sum_def fun_eq_iff sum_set_simps by auto
+
 subsection {* Transfer rules for the Transfer package *}
 
 context