diff -r 6ef5134fc631 -r 5257bc7e0c06 src/HOL/Induct/PropLog.thy
--- a/src/HOL/Induct/PropLog.thy	Sun Jun 01 17:45:43 2008 +0200
+++ b/src/HOL/Induct/PropLog.thy	Mon Jun 02 13:21:06 2008 +0200
@@ -134,14 +134,13 @@
 
 lemma false_imp: "H |- p->false ==> H |- p->q"
 apply (rule deduction)
-apply (erule weaken_left_insert [THEN thms_notE])
-apply blast
+apply (metis H insert_iff weaken_left_insert thms_notE)
 done
 
 lemma imp_false:
     "[| H |- p;  H |- q->false |] ==> H |- (p->q)->false"
 apply (rule deduction)
-apply (blast intro: weaken_left_insert thms.MP thms.H)
+apply (metis H MP insert_iff weaken_left_insert)
 done
 
 lemma hyps_thms_if: "hyps p tt |- (if tt[[p]] then p else p->false)"