1.1 --- a/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:14 2014 +0200
     1.2 +++ b/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:15 2014 +0200
     1.3 @@ -61,9 +61,9 @@
     1.4    shows "bi_unique (rel_prod R1 R2)"
     1.5    using assms unfolding bi_unique_def rel_prod_def by auto
     1.6  
     1.7 -lemma prod_invariant_commute [invariant_commute]: 
     1.8 -  "rel_prod (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (pred_prod P1 P2)"
     1.9 -  by (simp add: fun_eq_iff rel_prod_def pred_prod_def Lifting.invariant_def) blast
    1.10 +lemma prod_relator_eq_onp [relator_eq_onp]: 
    1.11 +  "rel_prod (eq_onp P1) (eq_onp P2) = eq_onp (pred_prod P1 P2)"
    1.12 +  by (simp add: fun_eq_iff rel_prod_def pred_prod_def eq_onp_def) blast
    1.13  
    1.14  subsection {* Quotient theorem for the Lifting package *}
    1.15