diff -r e1aa703c8cce -r 72cbbb4d98f3 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Fri Mar 25 13:52:23 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Mar 25 13:52:23 2022 +0100
@@ -128,40 +128,31 @@
   val bool_atype : (string * string) atp_type
   val individual_atype : (string * string) atp_type
   val mk_anot : ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula
-  val mk_aconn :
-    atp_connective -> ('a, 'b, 'c, 'd) atp_formula
-    -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula
+  val mk_aconn : atp_connective -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula ->
+    ('a, 'b, 'c, 'd) atp_formula
   val mk_app : (string, 'a) atp_term -> (string, 'a) atp_term -> (string, 'a) atp_term
   val mk_apps :  (string, 'a) atp_term -> (string, 'a) atp_term list -> (string, 'a) atp_term
   val mk_simple_aterm:  'a -> ('a, 'b) atp_term
-  val aconn_fold :
-    bool option -> (bool option -> 'a -> 'b -> 'b) -> atp_connective * 'a list
-    -> 'b -> 'b
-  val aconn_map :
-    bool option -> (bool option -> 'a -> ('b, 'c, 'd, 'e) atp_formula)
-    -> atp_connective * 'a list -> ('b, 'c, 'd, 'e) atp_formula
-  val formula_fold :
-    bool option -> (bool option -> 'c -> 'e -> 'e)
-    -> ('a, 'b, 'c, 'd) atp_formula -> 'e -> 'e
-  val formula_map :
-    ('c -> 'e) -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'e, 'd) atp_formula
+  val aconn_fold : bool option -> (bool option -> 'a -> 'b -> 'b) -> atp_connective * 'a list ->
+    'b -> 'b
+  val aconn_map : bool option -> (bool option -> 'a -> ('b, 'c, 'd, 'e) atp_formula) ->
+    atp_connective * 'a list -> ('b, 'c, 'd, 'e) atp_formula
+  val formula_fold : bool option -> (bool option -> 'c -> 'e -> 'e) ->
+    ('a, 'b, 'c, 'd) atp_formula -> 'e -> 'e
+  val formula_map : ('c -> 'e) -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'e, 'd) atp_formula
   val strip_atype : 'a atp_type -> 'a list * ('a atp_type list * 'a atp_type)
   val is_format_higher_order : atp_format -> bool
   val tptp_string_of_format : atp_format -> string
   val tptp_string_of_role : atp_formula_role -> string
   val tptp_string_of_line : atp_format -> string atp_problem_line -> string
-  val lines_of_atp_problem :
-    atp_format -> term_order -> (unit -> (string * int) list)
-    -> string atp_problem -> string list
-  val ensure_cnf_problem :
-    (string * string) atp_problem -> (string * string) atp_problem
-  val filter_cnf_ueq_problem :
-    (string * string) atp_problem -> (string * string) atp_problem
+  val lines_of_atp_problem : atp_format -> (unit -> (string * int) list) -> string atp_problem ->
+    string list
+  val ensure_cnf_problem : (string * string) atp_problem -> (string * string) atp_problem
+  val filter_cnf_ueq_problem : (string * string) atp_problem -> (string * string) atp_problem
   val declared_in_atp_problem : 'a atp_problem -> ('a list * 'a list) * 'a list
-  val nice_atp_problem :
-    bool -> atp_format -> ('a * (string * string) atp_problem_line list) list
-    -> ('a * string atp_problem_line list) list
-       * (string Symtab.table * string Symtab.table) option
+  val nice_atp_problem : bool -> atp_format ->
+    ('a * (string * string) atp_problem_line list) list ->
+    ('a * string atp_problem_line list) list * (string Symtab.table * string Symtab.table) option
 end;
 
 structure ATP_Problem : ATP_PROBLEM =
@@ -693,8 +684,14 @@
 fun maybe_enclose bef aft "" = "% " ^ bef ^ aft
   | maybe_enclose bef aft s = bef ^ s ^ aft
 
-fun dfg_lines poly {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem =
+fun dfg_lines poly ord_info problem =
   let
+    (* hardcoded settings *)
+    val is_lpo = false
+    val gen_weights = true
+    val gen_prec = true
+    val gen_simp = false
+
     val typ = string_of_type (DFG poly)
     val term = dfg_string_of_term
     fun spair (s, s') = "(" ^ s ^ ", " ^ s' ^ ")"
@@ -801,11 +798,11 @@
     ["end_problem.\n"]
   end
 
-fun lines_of_atp_problem format ord ord_info problem =
+fun lines_of_atp_problem format ord_info problem =
   "% This file was generated by Isabelle (most likely Sledgehammer)\n\
   \% " ^ timestamp () ^ "\n" ::
   (case format of
-     DFG poly => dfg_lines poly ord ord_info
+     DFG poly => dfg_lines poly ord_info
    | _ => tptp_lines format) problem