Fixed bug in function add_npvars.
authorberghofe
Sat Nov 03 18:49:40 2001 +0100 (2001-11-03)
changeset 1204127214c16ebe4
parent 12040 61e99f0f5c01
child 12042 1e5c01d5fe04
Fixed bug in function add_npvars.
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/proofterm.ML	Sat Nov 03 18:44:49 2001 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Sat Nov 03 18:49:40 2001 +0100
     1.3 @@ -755,12 +755,14 @@
     1.4        add_npvars q p Ts (add_npvars q (not p) Ts (vs, t), u)
     1.5    | add_npvars q p Ts (vs, Const ("all", Type (_, [Type (_, [T, _]), _])) $ t) =
     1.6        add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t)
     1.7 -  | add_npvars q p Ts (vs, t) = (case strip_comb t of
     1.8 +  | add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t)
     1.9 +  | add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t)
    1.10 +and add_npvars' Ts (vs, t) = (case strip_comb t of
    1.11      (Var (ixn, _), ts) => if test_args [] ts then vs
    1.12 -      else foldl (add_npvars q p Ts) (overwrite (vs,
    1.13 +      else foldl (add_npvars' Ts) (overwrite (vs,
    1.14          (ixn, foldl (add_funvars Ts) (if_none (assoc (vs, ixn)) [], ts))), ts)
    1.15 -  | (Abs (_, T, u), ts) => foldl (add_npvars q p (T::Ts)) (vs, u :: ts)
    1.16 -  | (_, ts) => foldl (add_npvars q p Ts) (vs, ts));
    1.17 +  | (Abs (_, T, u), ts) => foldl (add_npvars' (T::Ts)) (vs, u :: ts)
    1.18 +  | (_, ts) => foldl (add_npvars' Ts) (vs, ts));
    1.19  
    1.20  fun prop_vars (Const ("==>", _) $ P $ Q) = prop_vars P union prop_vars Q
    1.21    | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t