src/HOL/HOL.thy
changeset 15570 8d8c70b41bab
parent 15524 2ef571f80a55
child 15655 157f3988f775
     1.1 --- a/src/HOL/HOL.thy	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/HOL.thy	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -771,7 +771,7 @@
     1.4    fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
     1.5    |   wrong_prem (Bound _) = true
     1.6    |   wrong_prem _ = false
     1.7 -  val filter_right = filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t)))))
     1.8 +  val filter_right = List.filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t)))))
     1.9  in
    1.10    fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp])
    1.11    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]