src/HOL/Tools/ATP/atp_translate.ML

       | freeze (Var ((s, i), T)) =
         Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
       | freeze t = t
   in t |> exists_subterm is_Var t ? freeze end
 
-fun presimp_prop ctxt presimp_consts t =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val t = t |> Envir.beta_eta_contract
-              |> transform_elim_prop
-              |> Object_Logic.atomize_term thy
-    val need_trueprop = (fastype_of t = @{typ bool})
-  in
-    t |> need_trueprop ? HOLogic.mk_Trueprop
-      |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
-      |> extensionalize_term ctxt
-      |> presimplify_term ctxt presimp_consts
-      |> perhaps (try (HOLogic.dest_Trueprop))
-  end
+fun presimp_prop ctxt presimp_consts role t =
+  (let
+     val thy = Proof_Context.theory_of ctxt
+     val t = t |> Envir.beta_eta_contract
+               |> transform_elim_prop
+               |> Object_Logic.atomize_term thy
+     val need_trueprop = (fastype_of t = @{typ bool})
+   in
+     t |> need_trueprop ? HOLogic.mk_Trueprop
+       |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
+       |> extensionalize_term ctxt
+       |> presimplify_term ctxt presimp_consts
+       |> HOLogic.dest_Trueprop
+   end
+   handle TERM _ => if role = Conjecture then @{term False} else @{term True})
+  |> pair role
 
 (* making fact and conjecture formulas *)
 fun make_formula ctxt format type_enc eq_as_iff name loc kind t =
   let
     val (iformula, atomic_types) =

     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 = s_not t
+  | s_not_trueprop t =
+    if fastype_of t = @{typ bool} then s_not t else @{prop False} (* too meta *)
 
 fun make_conjecture ctxt format type_enc =
   map (fn ((name, loc), (kind, t)) =>
           t |> kind = Conjecture ? s_not_trueprop
             |> make_formula ctxt format type_enc (format <> CNF) name loc kind)

       |> map (apsnd freeze_term)
       |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
     val ((conjs, facts), lambdas) =
       if preproc then
         conjs @ facts
-        |> map (apsnd (apsnd (presimp_prop ctxt presimp_consts)))
+        |> map (apsnd (uncurry (presimp_prop ctxt presimp_consts)))
         |> preprocess_abstractions_in_terms trans_lambdas
         |>> chop (length conjs)
       else
         ((conjs, facts), [])
     val conjs = conjs |> make_conjecture ctxt format type_enc