# HG changeset patch
# User berghofe
# Date 1004809780 -3600
# Node ID 27214c16ebe406fdbf30c371bfb8cf7e33270223
# Parent  61e99f0f5c019458abff47530ecda7cd6f9cc9af
Fixed bug in function add_npvars.

diff -r 61e99f0f5c01 -r 27214c16ebe4 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Nov 03 18:44:49 2001 +0100
+++ b/src/Pure/proofterm.ML	Sat Nov 03 18:49:40 2001 +0100
@@ -755,12 +755,14 @@
       add_npvars q p Ts (add_npvars q (not p) Ts (vs, t), u)
   | add_npvars q p Ts (vs, Const ("all", Type (_, [Type (_, [T, _]), _])) $ t) =
       add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t)
-  | add_npvars q p Ts (vs, t) = (case strip_comb t of
+  | add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t)
+  | add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t)
+and add_npvars' Ts (vs, t) = (case strip_comb t of
     (Var (ixn, _), ts) => if test_args [] ts then vs
-      else foldl (add_npvars q p Ts) (overwrite (vs,
+      else foldl (add_npvars' Ts) (overwrite (vs,
         (ixn, foldl (add_funvars Ts) (if_none (assoc (vs, ixn)) [], ts))), ts)
-  | (Abs (_, T, u), ts) => foldl (add_npvars q p (T::Ts)) (vs, u :: ts)
-  | (_, ts) => foldl (add_npvars q p Ts) (vs, ts));
+  | (Abs (_, T, u), ts) => foldl (add_npvars' (T::Ts)) (vs, u :: ts)
+  | (_, ts) => foldl (add_npvars' Ts) (vs, ts));
 
 fun prop_vars (Const ("==>", _) $ P $ Q) = prop_vars P union prop_vars Q
   | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t