# HG changeset patch # User blanchet # Date 1328002144 -3600 # Node ID dce6c3a460a96a3f5a9c2a9207eebd464cf84500 # Parent 110ba63444462cfdc528c348cf35cabdca7ce01b new try at lambda-lifting that works correctly for both Metis and Sledgehammer (cf. d724066ff3d0) diff -r 110ba6344446 -r dce6c3a460a9 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jan 31 09:06:27 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jan 31 10:29:04 2012 +0100 @@ -1236,13 +1236,15 @@ if s = tptp_true then NONE else SOME formula | formula => SOME formula -fun s_not_trueprop (@{const Trueprop} \$ t) = @{const Trueprop} \$ s_not t - | s_not_trueprop t = - if fastype_of t = @{typ bool} then s_not t else @{prop False} (* too meta *) +fun not_trueprop (@{const Trueprop} \$ t) = + @{const Trueprop} \$ (@{const Not} \$ t) + | not_trueprop t = + if fastype_of t = @{typ bool} then @{const Not} \$ t + else @{prop False} (* "t" is too meta *) fun make_conjecture ctxt format type_enc = map (fn ((name, stature), (kind, t)) => - t |> kind = Conjecture ? s_not_trueprop + t |> kind = Conjecture ? not_trueprop |> make_formula ctxt format type_enc (format <> CNF) name stature kind) @@ -1729,7 +1731,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, s_not_trueprop concl_t)] + map (pair prem_kind) hyp_ts @ [(Conjecture, not_trueprop concl_t)] |> map (apsnd freeze_term) |> map2 (pair o rpair (Local, General) o string_of_int) (0 upto length hyp_ts)