src/HOL/Decision_Procs/ferrack_tac.ML
changeset 36692 54b64d4ad524
parent 35625 9c818cab0dd0
child 36853 c8e4102b08aa
     1.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4      val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
     1.5      val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
     1.6      fun mk_all ((s, T), (P,n)) =
     1.7 -      if 0 mem loose_bnos P then
     1.8 +      if member (op =) (loose_bnos P) 0 then
     1.9          (HOLogic.all_const T $ Abs (s, T, P), n)
    1.10        else (incr_boundvars ~1 P, n-1)
    1.11      fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;