# HG changeset patch
# User blanchet
# Date 1403022814 -7200
# Node ID 0260171a51ef3cc2db439f044379db4d720e9b39
# Parent  1df6f747f1643e091a1b95e35d1614ea59d13852
reintroduce atomize in Waldmeister code

diff -r 1df6f747f164 -r 0260171a51ef src/HOL/Tools/ATP/atp_waldmeister.ML
--- a/src/HOL/Tools/ATP/atp_waldmeister.ML	Tue Jun 17 16:02:49 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Tue Jun 17 18:33:34 2014 +0200
@@ -146,9 +146,13 @@
 
 fun generate_waldmeister_problem ctxt hyp_ts0 concl_t0 facts0 =
   let
-    val hyp_ts = map HOLogic.dest_Trueprop hyp_ts0
-    val concl_t = HOLogic.dest_Trueprop concl_t0
-    val facts = map (apsnd HOLogic.dest_Trueprop) facts0
+    val thy = Proof_Context.theory_of ctxt
+
+    val preproc = Object_Logic.atomize_term thy
+
+    val hyp_ts = map preproc hyp_ts0
+    val concl_t = preproc concl_t0
+    val facts = map (apsnd preproc) facts0
 
     val (conditions, consequence) = prepare_conjecture concl_t
     val fact_lines = maps (problem_lines_of_fact (fact_prefix ^ "0_" (* FIXME *))) facts
@@ -161,7 +165,7 @@
       if List.exists (is_eq o snd) facts orelse not (is_eq concl_t) then
         [(helpersN,
           @{thms waldmeister_fol}
-          |> map (fn th => (("", (Global, General)), HOLogic.dest_Trueprop (prop_of th)))
+          |> map (fn th => (("", (Global, General)), preproc (prop_of th)))
           |> maps (problem_lines_of_fact helper_prefix))]
       else
         []