src/HOL/TPTP/atp_theory_export.ML

                (case outcome of
                   NONE => "Success"
                 | SOME failure => string_of_atp_failure failure))
   in outcome end
 
-fun is_problem_line_reprovable ctxt format prelude axioms deps
-                               (Formula (ident', _, phi, _, _)) =
+fun is_problem_line_reprovable ctxt format prelude axioms deps (Formula (ident', _, phi, _, _)) =
     is_none (run_atp ctxt format
-        ((factsN, Formula (ident', Conjecture, phi, NONE, []) ::
-                  map_filter (Symtab.lookup axioms) deps) ::
-         prelude))
+      ((factsN,
+        Formula (ident', Conjecture, phi, NONE, []) :: map_filter (Symtab.lookup axioms) deps) ::
+       prelude))
   | is_problem_line_reprovable _ _ _ _ _ _ = false
 
 fun inference_term _ [] = NONE
   | inference_term check_infs ss =
     ATerm (("inference", []),

          ATerm ((tptp_empty_list, []),
          map (fn s => ATerm ((s, []), [])) ss)])
     |> SOME
 
 fun add_inferences_to_problem_line ctxt format check_infs prelude axioms infers
-        (line as Formula ((ident, alt), Axiom, phi, NONE, tms)) =
+      (line as Formula ((ident, alt), Axiom, phi, NONE, info)) =
     let
       val deps =
         case these (AList.lookup (op =) infers ident) of
           [] => []
         | deps =>

                                              line) then
             []
           else
             deps
     in
-      Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, tms)
+      Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, info)
     end
   | add_inferences_to_problem_line _ _ _ _ _ _ line = line
 
 fun add_inferences_to_problem ctxt format check_infs prelude infers problem =
   let

       |> sort (Sledgehammer_MaSh.crude_thm_ord ctxt o apply2 snd)
     val problem =
       facts
       |> map (fn ((_, loc), th) =>
         ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt))
-      |> generate_atp_problem ctxt format Axiom type_enc Exporter combsN false false true []
+      |> generate_atp_problem ctxt true format Axiom type_enc Exporter combsN false false true []
         @{prop False}
       |> #1 |> sort_by (heading_sort_key o fst)
     val prelude = fst (split_last problem)
     val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts
     val infers =

   "include('" ^ include_name ^ "/" ^ base_name ^ include_suffix ^ "').\n"
 
 val hol_base_name = encode_meta "HOL"
 
 fun should_generate_problem thy base_name (Formula ((_, alt), _, _, _, _)) =
-  case try (Global_Theory.get_thm thy) alt of
+  (case try (Global_Theory.get_thm thy) alt of
     SOME th =>
-    (* This is a crude hack to detect theorems stated and proved by the user (as
-       opposed to those derived by various packages). In addition, we leave out
-       everything in "HOL" as too basic to be interesting. *)
+    (* This is a crude hack to detect theorems stated and proved by the user (as opposed to those
+       derived by various packages). In addition, we leave out everything in "HOL" as too basic to
+       be interesting. *)
     Thm.legacy_get_kind th <> "" andalso base_name <> hol_base_name
-  | NONE => false
+  | NONE => false)
 
 (* Convention: theoryname__goalname *)
 fun problem_name_of base_name n alt =
   base_name ^ "__" ^ string_of_int n ^ "_" ^
   perhaps (try (unprefix (base_name ^ "_"))) alt ^ problem_suffix

       | write_problem_files n seen_facts includes _ ((base_name, []) :: groups) =
         write_problem_files n seen_facts (includes @ [include_line base_name]) [] groups
       | write_problem_files n seen_facts includes seen_ss
           ((base_name, fact_line :: fact_lines) :: groups) =
         let
-          val (ident, alt, pname, sname, conj) =
+          val (alt, pname, sname, conj) =
             (case fact_line of
               Formula ((ident, alt), _, phi, _, _) =>
-              (ident, alt, problem_name_of base_name n (encode_meta alt),
+              (alt, problem_name_of base_name n (encode_meta alt),
                suggestion_name_of base_name n (encode_meta alt),
                Formula ((ident, alt), Conjecture, phi, NONE, [])))
-
           val fact = the (Symtab.lookup fact_tab alt)
           val fact_s = tptp_string_of_line format fact_line
         in
           (if should_generate_problem thy base_name fact_line then
              let