src/HOL/Tools/ATP/atp_translate.ML
changeset 44460 5d0754cf994a
parent 44450 d848dd7b21f4
child 44463 c471a2b48fa1
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 24 10:59:22 2011 +0900
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 24 11:17:33 2011 +0200
     1.3 @@ -1059,16 +1059,14 @@
     1.4      | formula => SOME formula
     1.5    end
     1.6  
     1.7 -fun make_conjecture ctxt format type_enc ps =
     1.8 -  let
     1.9 -    val thy = Proof_Context.theory_of ctxt
    1.10 -    val last = length ps - 1
    1.11 -  in
    1.12 -    map2 (fn j => fn ((name, loc), (kind, t)) =>
    1.13 -             t |> make_formula thy type_enc (format <> CNF) name loc kind
    1.14 -               |> (j <> last) = (kind = Conjecture) ? update_iformula mk_anot)
    1.15 -         (0 upto last) ps
    1.16 -  end
    1.17 +fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
    1.18 +  | s_not_trueprop t = s_not t
    1.19 +
    1.20 +fun make_conjecture thy format type_enc ps =
    1.21 +  map2 (fn j => fn ((name, loc), (kind, t)) =>
    1.22 +           t |> kind = Conjecture ? s_not_trueprop
    1.23 +             |> make_formula thy type_enc (format <> CNF) name loc kind)
    1.24 +       (0 upto length ps - 1) ps
    1.25  
    1.26  (** Finite and infinite type inference **)
    1.27  
    1.28 @@ -1552,7 +1550,7 @@
    1.29        |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
    1.30      val facts = facts |> map (apsnd (pair Axiom))
    1.31      val conjs =
    1.32 -      map (pair prem_kind) hyp_ts @ [(Conjecture, concl_t)]
    1.33 +      map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
    1.34        |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
    1.35      val ((conjs, facts), lambdas) =
    1.36        if preproc then
    1.37 @@ -1563,7 +1561,7 @@
    1.38          |>> apfst (map (apsnd (apsnd freeze_term)))
    1.39        else
    1.40          ((conjs, facts), [])
    1.41 -    val conjs = conjs |> make_conjecture ctxt format type_enc
    1.42 +    val conjs = conjs |> make_conjecture thy format type_enc
    1.43      val (fact_names, facts) =
    1.44        facts
    1.45        |> map_filter (fn (name, (_, t)) =>