1.1 --- a/src/HOL/UNITY/PPROD.thy	Tue Feb 21 17:08:32 2012 +0100
     1.2 +++ b/src/HOL/UNITY/PPROD.thy	Tue Feb 21 17:09:17 2012 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4  by (simp add: PLam_def)
     1.5  
     1.6  lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
     1.7 -by (simp add: PLam_def lift_SKIP JN_constant)
     1.8 +by (simp add: PLam_def JN_constant)
     1.9  
    1.10  lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
    1.11  by (unfold PLam_def, auto)