# HG changeset patch
# User steckerm
# Date 1413287498 -7200
# Node ID 97c6818f46969fbe4f015f96c91ddf7af96ccdf8
# Parent  6bade3d91c496b3793bd2f3c5fe5ae4171ac8e1b
Fixed bug in waldmeister skolemization

diff -r 6bade3d91c49 -r 97c6818f4696 src/HOL/Tools/ATP/atp_waldmeister.ML
--- 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