src/HOL/Tools/ATP/atp_problem_generate.ML

                          name stature Axiom of
     formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
     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)
 
 (** Finite and infinite type inference **)
 

     val hyp_ts =
       hyp_ts
       |> 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)
     val ((conjs, facts), lam_facts) =
       (conjs, facts)