new try at lambda-lifting that works correctly for both Metis and Sledgehammer (cf. d724066ff3d0)

--- 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)