src/Pure/proofterm.ML

--- a/src/Pure/proofterm.ML	Wed Oct 04 11:50:37 2006 +0200
+++ b/src/Pure/proofterm.ML	Wed Oct 04 14:14:33 2006 +0200
@@ -889,7 +889,8 @@
   end;
 
 fun needed_vars prop = 
-  Library.foldl op union ([], map op ins (add_npvars true true [] ([], prop))) union
+  Library.foldl (op union)
+    ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))) union
   prop_vars prop;
 
 fun gen_axm_proof c name prop =