src/HOL/Tools/ATP/atp_problem_generate.ML

           else
             fact :: reorder [] (facts @ skipped)
         end
   in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end
 
+fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
+  | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
+  | s_not_prop t = @{const "==>"} $ t $ @{prop False}
+
 fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts
                        concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt
     val trans_lams = trans_lams_of_string ctxt type_enc lam_trans