new proof of drop_prog_correct for new definition of project_act

--- a/src/HOL/UNITY/Lift_prog.ML	Tue Sep 21 11:09:24 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML	Tue Sep 21 11:11:09 1999 +0200
@@ -245,8 +245,10 @@
 by (rtac program_equalityI 1);
 by (simp_tac (simpset() addsimps [drop_set_correct]) 1);
 by (simp_tac (simpset() 
-	      addsimps [lift_export Acts_project,
-			drop_act_correct]) 1);
+	      addsimps [Acts_project, drop_act_correct]) 1);
+by (rtac (insert_absorb RS sym) 1);
+by (rtac (Id_in_Acts RSN (2,image_eqI)) 1);
+by (rtac (project_set_UNIV RS lift_export project_act_Id RS sym) 1);
 qed "drop_prog_correct";