--- a/src/HOL/UNITY/PPROD.ML	Thu Mar 22 10:29:26 2001 +0100
+++ b/src/HOL/UNITY/PPROD.ML	Fri Mar 23 10:10:53 2001 +0100
@@ -103,7 +103,6 @@
 \     ==> (PLam I F : preserves (v o sub j o fst)) = \
 \         (if j: I then F j : preserves (v o fst) else True)";
 by (asm_simp_tac (simpset() addsimps [PLam_def, lift_preserves_sub]) 1);
-by (Blast_tac 1);
 qed "PLam_preserves_fst";
 Addsimps [PLam_preserves_fst];