# HG changeset patch
# User steckerm
# Date 1411202528 -7200
# Node ID 623645fdb0472ffbcd6021cf543ee87cc4710f52
# Parent  b8ca69d9897b56bea32b797173592101c843b12c
Improved equality handling in skolemization

diff -r b8ca69d9897b -r 623645fdb047 src/HOL/Tools/ATP/atp_waldmeister.ML
--- 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;