--- a/src/HOL/Tools/ATP/atp_waldmeister.ML Tue Oct 14 10:52:46 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML Tue Oct 14 13:51:38 2014 +0200
@@ -131,10 +131,13 @@
else
(ctxt1,ctxt2,spets,c $ a $ b)
| skolemize' _ ctxt1 ctxt2 spets _ trm = (ctxt1, ctxt2, spets, trm)
+
+ fun vars_of trm =
+ rev (distinct (op =) (Term.fold_aterms (fn t as Var _ => cons t | _ => I) trm []));
fun skolemize positve ctxt trm =
let
- val (ctxt1, _, spets, skolemized_trm) = skolemize' positve ctxt ctxt [] [] trm
+ val (ctxt1, _, spets, skolemized_trm) = skolemize' positve ctxt ctxt [] (vars_of trm) trm
in
(ctxt1, (trm :: List.rev spets, skolemized_trm))
end