diff -r ae9286f64574 -r e5438c5797ae src/HOL/UNITY/PPROD.thy
--- a/src/HOL/UNITY/PPROD.thy	Tue Feb 21 17:08:32 2012 +0100
+++ b/src/HOL/UNITY/PPROD.thy	Tue Feb 21 17:09:17 2012 +0100
@@ -29,7 +29,7 @@
 by (simp add: PLam_def)
 
 lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
-by (simp add: PLam_def lift_SKIP JN_constant)
+by (simp add: PLam_def JN_constant)
 
 lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
 by (unfold PLam_def, auto)