src/HOL/HOL_lemmas.ML
changeset 7533 1659dc4e3552
parent 7490 9a74b57740d1
child 7560 19c3be2d285c
--- a/src/HOL/HOL_lemmas.ML	Thu Sep 09 13:24:26 1999 +0200
+++ b/src/HOL/HOL_lemmas.ML	Thu Sep 09 14:30:08 1999 +0200
@@ -429,9 +429,7 @@
   fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
   |   wrong_prem (Bound _) = true
   |   wrong_prem _ = false;
-  fun wrong (Const ("==>", _) $ (Const ("Trueprop", _) $ t) $ _) = wrong_prem t
-  |   wrong _ = true;
-  val filter_right = filter (fn t => not (wrong (#prop (rep_thm t))));
+  val filter_right = filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t)))));
 in
   fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
   fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]