# HG changeset patch
# User oheimb
# Date 936880208 -7200
# Node ID 1659dc4e35527e57e7e9df29a05524baa9e2dcbd
# Parent  a77d5feec30434aa26ce07b9bbe6322a133556f5
minor change to smp_tac

diff -r a77d5feec304 -r 1659dc4e3552 src/HOL/HOL_lemmas.ML
--- 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]