--- a/src/HOL/Tools/ATP/atp_waldmeister.ML Sat Sep 20 10:42:08 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML Sat Sep 20 10:42:08 2014 +0200
@@ -100,8 +100,8 @@
in
(ctxt1',ctxt2',map mk_not spets',mk_not trm'')
end
- | skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (@{const_name HOL.eq},_) $ a $ b)) =
- if contains_quantor trm then
+ | skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (@{const_name HOL.eq},t) $ a $ b)) =
+ if contains_quantor trm andalso t = @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"}then
skolemize' pos ctxt1 ctxt2 (trm::spets) vars (mk_conj (mk_imp (a,b), mk_imp (b,a)))
else
(ctxt1,ctxt2,spets,trm)
@@ -494,4 +494,4 @@
fun introduce_waldmeister_skolems info (proof_steps : (term, string) atp_step list) = proof_steps
|> map (skolemization_steps info) |> List.concat
-end;
\ No newline at end of file
+end;