cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer

--- a/src/HOL/TPTP/atp_problem_import.ML	Sat Dec 19 20:02:51 2015 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Sat Dec 19 20:02:51 2015 +0100
@@ -315,6 +315,7 @@
       | "DFG" => (DFG Monomorphic, "mono_native", liftingN)
       | _ => error ("Unknown format " ^ quote format_str ^
         " (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")"))
+    val generate_info = false
     val uncurried_aliases = false
     val readable_names = true
     val presimp = true
@@ -322,7 +323,8 @@
       map (apfst (rpair (Global, Non_Rec_Def))) defs @
       map (apfst (rpair (Global, General))) nondefs
     val (atp_problem, _, _, _) =
-      generate_atp_problem ctxt format Hypothesis (type_enc_of_string Strict type_enc) Translator
+      generate_atp_problem ctxt generate_info format Hypothesis (type_enc_of_string Strict type_enc)
+        Translator
         lam_trans uncurried_aliases readable_names presimp [] conj facts
 
     val ord = effective_term_order ctxt spassN

--- a/src/HOL/TPTP/atp_theory_export.ML	Sat Dec 19 20:02:51 2015 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML	Sat Dec 19 20:02:51 2015 +0100
@@ -75,12 +75,11 @@
                 | 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
@@ -93,7 +92,7 @@
     |> 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
@@ -106,7 +105,7 @@
           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
 
@@ -170,7 +169,7 @@
       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)
@@ -269,13 +268,13 @@
 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 =
@@ -342,13 +341,12 @@
       | 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

--- a/src/HOL/Tools/ATP/atp_problem.ML	Sat Dec 19 20:02:51 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sat Dec 19 20:02:51 2015 +0100
@@ -98,7 +98,7 @@
   val tptp_empty_list : string
   val dfg_individual_type : string
   val isabelle_info_prefix : string
-  val isabelle_info : string -> int -> (string, 'a) atp_term list
+  val isabelle_info : bool -> string -> int -> (string, 'a) atp_term list
   val extract_isabelle_status : (string, 'a) atp_term list -> string option
   val extract_isabelle_rank : (string, 'a) atp_term list -> int
   val inductionN : string
@@ -138,6 +138,7 @@
     ('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_line : atp_format -> string atp_problem_line -> string
   val lines_of_atp_problem :
     atp_format -> term_order -> (unit -> (string * int) list)
@@ -271,12 +272,16 @@
 val default_rank = 1000
 val default_term_order_weight = 1
 
-(* Currently, only SPASS 3.8ds can process Isabelle metainformation. *)
-fun isabelle_info status rank =
-  [] |> rank <> default_rank
-        ? cons (ATerm ((isabelle_info_prefix ^ rankN, []),
-                       [ATerm ((string_of_int rank, []), [])]))
-     |> status <> "" ? cons (ATerm ((isabelle_info_prefix ^ status, []), []))
+(* Currently, only SPASS 3.8ds and (to a lesser extent) Metis can process Isabelle
+   metainformation. *)
+fun isabelle_info generate_info status rank =
+  if generate_info then
+    [] |> rank <> default_rank
+          ? cons (ATerm ((isabelle_info_prefix ^ rankN, []),
+                         [ATerm ((string_of_int rank, []), [])]))
+       |> status <> "" ? cons (ATerm ((isabelle_info_prefix ^ status, []), []))
+  else
+    []
 
 fun extract_isabelle_status (ATerm ((s, []), []) :: _) =
     try (unprefix isabelle_info_prefix) s
@@ -542,13 +547,16 @@
   | tptp_string_of_line format (Sym_Decl (ident, sym, ty)) =
     tptp_string_of_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^
     " : " ^ string_of_type format ty ^ ").\n"
-  | tptp_string_of_line format (Formula ((ident, alt), kind, phi, source, _)) =
+  | tptp_string_of_line format (Formula ((ident, alt), kind, phi, source, info)) =
     tptp_string_of_format format ^ "(" ^ ident ^ ", " ^
     tptp_string_of_role kind ^ "," ^ "\n    (" ^
     tptp_string_of_formula format phi ^ ")" ^
     (case source of
       SOME tm => ", " ^ tptp_string_of_term format tm
-    | NONE => "") ^
+    | NONE => if null info then "" else ", []") ^
+    (case info of
+      [] => ""
+    | tms => ", [" ^ commas (map (tptp_string_of_term format) tms) ^ "]") ^
     ")." ^ maybe_alt alt ^ "\n"
 
 fun tptp_lines format =

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Dec 19 20:02:51 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Dec 19 20:02:51 2015 +0100
@@ -112,9 +112,10 @@
     Proof.context -> type_enc -> string -> term list -> term list * term list
   val string_of_status : status -> string
   val factsN : string
-  val generate_atp_problem : Proof.context -> atp_format -> atp_formula_role -> type_enc -> mode ->
-    string -> bool -> bool -> bool -> term list -> term -> ((string * stature) * term) list ->
-    string atp_problem * string Symtab.table * (string * term) list * int Symtab.table
+  val generate_atp_problem : Proof.context -> bool -> atp_format -> atp_formula_role -> type_enc ->
+    mode -> string -> bool -> bool -> bool -> term list -> term ->
+    ((string * stature) * term) list -> string atp_problem * string Symtab.table
+    * (string * term) list * int Symtab.table
   val atp_problem_selection_weights : string atp_problem -> (string * real) list
   val atp_problem_term_order_info : string atp_problem -> (string * int) list
 end;
@@ -2017,7 +2018,7 @@
 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    of monomorphization). The TPTP forbids name clashes, and some of the remote
    provers might care. *)
-fun line_of_fact ctxt prefix encode alt freshen pos mono type_enc rank
+fun line_of_fact ctxt generate_info prefix encode alt freshen pos mono type_enc rank
         (j, {name, stature = (_, status), role, iformula, atomic_types}) =
   Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
             encode name, alt name),
@@ -2027,23 +2028,22 @@
                   should_guard_var_in_formula (if pos then SOME true else NONE)
            |> close_formula_universally
            |> bound_tvars type_enc true atomic_types,
-           NONE, isabelle_info (string_of_status status) (rank j))
+           NONE, isabelle_info generate_info (string_of_status status) (rank j))
 
-fun lines_of_subclass type_enc sub super =
+fun lines_of_subclass generate_info type_enc sub super =
   Formula ((subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, ""), Axiom,
            AConn (AImplies,
                   [sub, super] |> map (fn s => class_atom type_enc (s, tvar_a)))
            |> bound_tvars type_enc false [tvar_a],
-           NONE, isabelle_info inductiveN helper_rank)
+           NONE, isabelle_info generate_info inductiveN helper_rank)
 
-fun lines_of_subclass_pair type_enc (sub, supers) =
+fun lines_of_subclass_pair generate_info type_enc (sub, supers) =
   if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
-    [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub,
-                 map (`make_class) supers)]
+    [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub, map (`make_class) supers)]
   else
-    map (lines_of_subclass type_enc sub) supers
+    map (lines_of_subclass generate_info type_enc sub) supers
 
-fun line_of_tcon_clause type_enc (name, prems, (cl, T)) =
+fun line_of_tcon_clause generate_info type_enc (name, prems, (cl, T)) =
   if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
     Class_Memb (class_memb_prefix ^ name,
       map (fn (cls, T) => (T |> dest_TVar |> tvar_name, map (`make_class) cls)) prems,
@@ -2053,14 +2053,12 @@
              mk_ahorn (maps (class_atoms type_enc) prems)
                       (class_atom type_enc (cl, T))
              |> bound_tvars type_enc true (snd (dest_Type T)),
-             NONE, isabelle_info inductiveN helper_rank)
+             NONE, isabelle_info generate_info inductiveN helper_rank)
 
-fun line_of_conjecture ctxt mono type_enc
-                       ({name, role, iformula, atomic_types, ...} : ifact) =
+fun line_of_conjecture ctxt mono type_enc ({name, role, iformula, atomic_types, ...} : ifact) =
   Formula ((conjecture_prefix ^ name, ""), role,
            iformula
-           |> formula_of_iformula ctxt mono type_enc
-                  should_guard_var_in_formula (SOME false)
+           |> formula_of_iformula ctxt mono type_enc should_guard_var_in_formula (SOME false)
            |> close_formula_universally
            |> bound_tvars type_enc true atomic_types, NONE, [])
 
@@ -2230,7 +2228,7 @@
           ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
   end
 
-fun line_of_guards_mono_type ctxt mono type_enc T =
+fun line_of_guards_mono_type ctxt generate_info mono type_enc T =
   Formula ((guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""),
            Axiom,
            IConst (`make_bound_var "X", T, [])
@@ -2240,21 +2238,21 @@
                                   (SOME true)
            |> close_formula_universally
            |> bound_tvars type_enc true (atomic_types_of T),
-           NONE, isabelle_info inductiveN helper_rank)
+           NONE, isabelle_info generate_info inductiveN helper_rank)
 
-fun line_of_tags_mono_type ctxt mono type_enc T =
+fun line_of_tags_mono_type ctxt generate_info mono type_enc T =
   let val x_var = ATerm ((`make_bound_var "X", []), []) in
     Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom,
              eq_formula type_enc (atomic_types_of T) [] false
                   (tag_with_type ctxt mono type_enc NONE T x_var) x_var,
-             NONE, isabelle_info non_rec_defN helper_rank)
+             NONE, isabelle_info generate_info non_rec_defN helper_rank)
   end
 
-fun lines_of_mono_types ctxt mono type_enc =
+fun lines_of_mono_types ctxt generate_info mono type_enc =
   (case type_enc of
     Native _ => K []
-  | Guards _ => map (line_of_guards_mono_type ctxt mono type_enc)
-  | Tags _ => map (line_of_tags_mono_type ctxt mono type_enc))
+  | Guards _ => map (line_of_guards_mono_type ctxt generate_info mono type_enc)
+  | Tags _ => map (line_of_tags_mono_type ctxt generate_info mono type_enc))
 
 fun decl_line_of_sym ctxt mono type_enc s (s', T_args, T, pred_sym, ary, _) =
   let
@@ -2280,8 +2278,8 @@
 
 fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I)
 
-fun line_of_guards_sym_decl ctxt mono type_enc n s j
-                            (s', T_args, T, _, ary, in_conj) =
+fun line_of_guards_sym_decl ctxt generate_info mono type_enc n s j
+    (s', T_args, T, _, ary, in_conj) =
   let
     val thy = Proof_Context.theory_of ctxt
     val (role, maybe_negate) = honor_conj_sym_role in_conj
@@ -2310,11 +2308,11 @@
              |> close_formula_universally
              |> bound_tvars type_enc (n > 1) (atomic_types_of T)
              |> maybe_negate,
-             NONE, isabelle_info inductiveN helper_rank)
+             NONE, isabelle_info generate_info inductiveN helper_rank)
   end
 
-fun lines_of_tags_sym_decl ctxt mono type_enc n s
-                           (j, (s', T_args, T, pred_sym, ary, in_conj)) =
+fun lines_of_tags_sym_decl ctxt generate_info mono type_enc n s
+    (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   let
     val thy = Proof_Context.theory_of ctxt
     val level = level_of_type_enc type_enc
@@ -2330,7 +2328,7 @@
     val tag_with = tag_with_type ctxt mono type_enc NONE
     fun formula c =
       [Formula ((ident, ""), role, eq (tag_with res_T c) c, NONE,
-                isabelle_info non_rec_defN helper_rank)]
+                isabelle_info generate_info non_rec_defN helper_rank)]
   in
     if pred_sym orelse not (should_encode_type ctxt mono level res_T) then
       []
@@ -2355,7 +2353,7 @@
     end
   | rationalize_decls _ decls = decls
 
-fun lines_of_sym_decls ctxt mono type_enc (s, decls) =
+fun lines_of_sym_decls ctxt generate_info mono type_enc (s, decls) =
   (case type_enc of
     Native _ => [decl_line_of_sym ctxt mono type_enc s (hd decls)]
   | Guards (_, level) =>
@@ -2365,21 +2363,23 @@
       val n = length decls
       val decls = decls |> filter (should_encode_type ctxt mono level o result_type_of_decl)
     in
-      (0 upto length decls - 1, decls) |-> map2 (line_of_guards_sym_decl ctxt mono type_enc n s)
+      (0 upto length decls - 1, decls)
+      |-> map2 (line_of_guards_sym_decl ctxt generate_info mono type_enc n s)
     end
   | Tags (_, level) =>
     if is_type_level_uniform level then
       []
     else
       let val n = length decls in
-        (0 upto n - 1 ~~ decls) |> maps (lines_of_tags_sym_decl ctxt mono type_enc n s)
+        (0 upto n - 1 ~~ decls)
+        |> maps (lines_of_tags_sym_decl ctxt generate_info mono type_enc n s)
       end)
 
-fun lines_of_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab =
+fun lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts sym_decl_tab =
   let
     val syms = sym_decl_tab |> Symtab.dest |> sort_by fst
-    val mono_lines = lines_of_mono_types ctxt mono type_enc mono_Ts
-    val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms
+    val mono_lines = lines_of_mono_types ctxt generate_info mono type_enc mono_Ts
+    val decl_lines = maps (lines_of_sym_decls ctxt generate_info mono type_enc) syms
   in mono_lines @ decl_lines end
 
 fun datatypes_of_sym_table ctxt ctrss (DFG Polymorphic) (type_enc as Native _) uncurried_aliases
@@ -2426,8 +2426,8 @@
 
 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
 
-fun do_uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab
-                                    base_s0 types in_conj =
+fun do_uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab base_s0
+    types in_conj =
   let
     fun do_alias ary =
       let
@@ -2464,31 +2464,32 @@
       in
         ([tm1, tm2],
          [Formula ((uncurried_alias_eq_prefix ^ s2, ""), role, eq |> maybe_negate, NONE,
-            isabelle_info non_rec_defN helper_rank)])
+            isabelle_info generate_info non_rec_defN helper_rank)])
         |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
             else pair_append (do_alias (ary - 1)))
       end
   in do_alias end
 
-fun uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab
+fun uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab
         (s, {min_ary, types, in_conj, ...} : sym_info) =
   (case unprefix_and_unascii const_prefix s of
     SOME mangled_s =>
     if String.isSubstring uncurried_alias_sep mangled_s then
       let val base_s0 = mangled_s |> unmangled_invert_const in
-        do_uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab base_s0 types
-          in_conj min_ary
+        do_uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab
+          base_s0 types in_conj min_ary
       end
     else
       ([], [])
   | NONE => ([], []))
 
-fun uncurried_alias_lines_of_sym_table ctxt ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab =
+fun uncurried_alias_lines_of_sym_table ctxt generate_info ctrss mono type_enc uncurried_aliases
+    sym_tab0 sym_tab =
   ([], [])
   |> uncurried_aliases
-    ? Symtab.fold_rev
-        (pair_append o uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab)
-        sym_tab
+    ? Symtab.fold_rev (pair_append
+        o uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab)
+      sym_tab
 
 val implicit_declsN = "Could-be-implicit typings"
 val explicit_declsN = "Explicit typings"
@@ -2563,8 +2564,8 @@
 
 val app_op_and_predicator_threshold = 45
 
-fun generate_atp_problem ctxt format prem_role type_enc mode lam_trans uncurried_aliases
-    readable_names presimp hyp_ts concl_t facts =
+fun generate_atp_problem ctxt generate_info format prem_role type_enc mode lam_trans
+    uncurried_aliases readable_names presimp hyp_ts concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt
     val type_enc = type_enc |> adjust_type_enc format
@@ -2595,7 +2596,8 @@
     val (ho_stuff, sym_tab) =
       sym_table_of_facts ctxt type_enc Min_App_Op conjs facts
     val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
-      uncurried_alias_lines_of_sym_table ctxt ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab
+      uncurried_alias_lines_of_sym_table ctxt generate_info ctrss mono type_enc uncurried_aliases
+        sym_tab0 sym_tab
     val (_, sym_tab) =
       (ho_stuff, sym_tab)
       |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false)
@@ -2610,7 +2612,7 @@
     val sym_decl_lines =
       (conjs, helpers @ facts, uncurried_alias_eq_tms)
       |> sym_decl_table_of_facts thy type_enc sym_tab
-      |> lines_of_sym_decl_table ctxt mono type_enc mono_Ts
+      |> lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts
     val datatype_decl_lines = map decl_line_of_datatype datatypes
     val decl_lines = class_decl_lines @ sym_decl_lines @ datatype_decl_lines
     val num_facts = length facts
@@ -2618,13 +2620,14 @@
     val pos = mode <> Exporter
     val rank_of = rank_of_fact_num num_facts
     val fact_lines =
-      map (line_of_fact ctxt fact_prefix ascii_of I freshen pos mono type_enc rank_of)
+      map (line_of_fact ctxt generate_info fact_prefix ascii_of I freshen pos mono type_enc rank_of)
         (0 upto num_facts - 1 ~~ facts)
-    val subclass_lines = maps (lines_of_subclass_pair type_enc) subclass_pairs
-    val tcon_lines = map (line_of_tcon_clause type_enc) tcon_clauses
+    val subclass_lines = maps (lines_of_subclass_pair generate_info type_enc) subclass_pairs
+    val tcon_lines = map (line_of_tcon_clause generate_info type_enc) tcon_clauses
     val helper_lines =
       0 upto length helpers - 1 ~~ helpers
-      |> map (line_of_fact ctxt helper_prefix I (K "") false true mono type_enc (K default_rank))
+      |> map (line_of_fact ctxt generate_info helper_prefix I (K "") false true mono type_enc
+        (K default_rank))
     val free_type_lines = lines_of_free_types type_enc (facts @ conjs)
     val conj_lines = map (line_of_conjecture ctxt mono type_enc) conjs
     (* Reordering these might confuse the proof reconstruction code. *)

--- a/src/HOL/Tools/Metis/metis_generate.ML	Sat Dec 19 20:02:51 2015 +0100
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Sat Dec 19 20:02:51 2015 +0100
@@ -227,7 +227,7 @@
     *)
     val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
     val (atp_problem, _, lifted, sym_tab) =
-      generate_atp_problem ctxt CNF Hypothesis type_enc Metis lam_trans false false false []
+      generate_atp_problem ctxt true CNF Hypothesis type_enc Metis lam_trans false false false []
         @{prop False} props
     (*
     val _ = tracing ("ATP PROBLEM: " ^

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Dec 19 20:02:51 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Dec 19 20:02:51 2015 +0100
@@ -235,6 +235,7 @@
             val num_facts =
               Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge
               |> Integer.min (length facts)
+            val generate_info = (case format of DFG _ => true | _ => false)
             val strictness = if strict then Strict else Non_Strict
             val type_enc = type_enc |> choose_type_enc strictness best_type_enc format
             val sound = is_type_enc_sound type_enc
@@ -273,8 +274,8 @@
                       generate_waldmeister_problem ctxt hyp_ts concl_t
                       #> (fn (a, b, c, d, e) => (a, b, c, d, SOME e))
                     else
-                      generate_atp_problem ctxt format prem_role type_enc atp_mode lam_trans
-                        uncurried_aliases readable_names true hyp_ts concl_t
+                      generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode
+                        lam_trans uncurried_aliases readable_names true hyp_ts concl_t
                       #> (fn (a, b, c, d) => (a, b, c, d, NONE)))
 
             fun sel_weights () = atp_problem_selection_weights atp_problem