# HG changeset patch
# User blanchet
# Date 1314177453 -7200
# Node ID 5d0754cf994a7c688f72247020b103a9717dd449
# Parent  079ccfb074d95a26ce839947398e8e325279329b
tuning

diff -r 079ccfb074d9 -r 5d0754cf994a src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 24 10:59:22 2011 +0900
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 24 11:17:33 2011 +0200
@@ -1059,16 +1059,14 @@
     | formula => SOME formula
   end
 
-fun make_conjecture ctxt format type_enc ps =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val last = length ps - 1
-  in
-    map2 (fn j => fn ((name, loc), (kind, t)) =>
-             t |> make_formula thy type_enc (format <> CNF) name loc kind
-               |> (j <> last) = (kind = Conjecture) ? update_iformula mk_anot)
-         (0 upto last) ps
-  end
+fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
+  | s_not_trueprop t = s_not t
+
+fun make_conjecture thy format type_enc ps =
+  map2 (fn j => fn ((name, loc), (kind, t)) =>
+           t |> kind = Conjecture ? s_not_trueprop
+             |> make_formula thy type_enc (format <> CNF) name loc kind)
+       (0 upto length ps - 1) ps
 
 (** Finite and infinite type inference **)
 
@@ -1552,7 +1550,7 @@
       |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
     val facts = facts |> map (apsnd (pair Axiom))
     val conjs =
-      map (pair prem_kind) hyp_ts @ [(Conjecture, concl_t)]
+      map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
       |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
     val ((conjs, facts), lambdas) =
       if preproc then
@@ -1563,7 +1561,7 @@
         |>> apfst (map (apsnd (apsnd freeze_term)))
       else
         ((conjs, facts), [])
-    val conjs = conjs |> make_conjecture ctxt format type_enc
+    val conjs = conjs |> make_conjecture thy format type_enc
     val (fact_names, facts) =
       facts
       |> map_filter (fn (name, (_, t)) =>
diff -r 079ccfb074d9 -r 5d0754cf994a src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Wed Aug 24 10:59:22 2011 +0900
+++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Aug 24 11:17:33 2011 +0200
@@ -272,7 +272,7 @@
 
 (* Converts an elim-rule into an equivalent theorem that does not have the
    predicate variable. Leaves other theorems unchanged. We simply instantiate
-   the conclusion variable to False. (Cf. "transform_elim_theorem" in
+   the conclusion variable to "False". (Cf. "transform_elim_theorem" in
    "Meson_Clausify".) *)
 fun transform_elim_prop t =
   case Logic.strip_imp_concl t of