# HG changeset patch
# User blanchet
# Date 1292408789 -3600
# Node ID 7e90d259790bbdf887fe34d25c5889c8803e940f
# Parent  9aeaf8acf6c864d4412d555b368e31f751113413
tuning

diff -r 9aeaf8acf6c8 -r 7e90d259790b src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:29 2010 +0100
@@ -337,7 +337,7 @@
       else make_arity_clauses thy tycons supers
     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   in
-    (fact_names |> map single |> Vector.fromList,
+    (fact_names |> map single,
      (conjectures, facts, class_rel_clauses, arity_clauses))
   end
 
@@ -612,49 +612,50 @@
 
 fun dest_Fof (Fof z) = z
 
+val factsN = "Relevant facts"
+val class_relsN = "Class relationships"
+val aritiesN = "Arity declarations"
+val helpersN = "Helper facts"
+val conjsN = "Conjectures"
+val tfreesN = "Type variables"
+
+fun offset_of_heading_in_problem _ [] j = j
+  | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
+    if heading = needle then j
+    else offset_of_heading_in_problem needle problem (j + length lines)
+
 fun prepare_atp_problem ctxt readable_names explicit_forall type_sys
                         explicit_apply hyp_ts concl_t facts =
   let
     val thy = ProofContext.theory_of ctxt
     val (fact_names, (conjectures, facts, class_rel_clauses, arity_clauses)) =
       translate_formulas ctxt type_sys hyp_ts concl_t facts
-    val fact_lines = map (problem_line_for_fact ctxt fact_prefix type_sys) facts
-    val conjecture_lines =
-      map (problem_line_for_conjecture ctxt type_sys) conjectures
-    val tfree_lines = problem_lines_for_free_types type_sys conjectures
-    val class_rel_lines =
-      map problem_line_for_class_rel_clause class_rel_clauses
-    val arity_lines = map problem_line_for_arity_clause arity_clauses
     (* Reordering these might or might not confuse the proof reconstruction
        code or the SPASS Flotter hack. *)
     val problem =
-      [("Relevant facts", fact_lines),
-       ("Class relationships", class_rel_lines),
-       ("Arity declarations", arity_lines),
-       ("Helper facts", []),
-       ("Conjectures", conjecture_lines),
-       ("Type variables", tfree_lines)]
+      [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys) facts),
+       (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses),
+       (aritiesN, map problem_line_for_arity_clause arity_clauses),
+       (helpersN, []),
+       (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjectures),
+       (tfreesN, problem_lines_for_free_types type_sys conjectures)]
     val const_tab = const_table_for_problem explicit_apply problem
     val problem =
       problem |> repair_problem thy explicit_forall type_sys const_tab
-    val (helper_facts, raw_helper_lines) =
+    val helper_lines =
       get_helper_facts ctxt explicit_forall type_sys
                        (maps (map (#3 o dest_Fof) o snd) problem)
-    val helper_lines =
-      (helper_facts
-       |> map (problem_line_for_fact ctxt helper_prefix type_sys
-               #> repair_problem_line thy explicit_forall type_sys const_tab)) @
-      raw_helper_lines
+      |>> map (problem_line_for_fact ctxt helper_prefix type_sys
+               #> repair_problem_line thy explicit_forall type_sys const_tab)
+      |> op @
     val (problem, pool) =
-      problem |> AList.update (op =) ("Helper facts", helper_lines)
+      problem |> AList.update (op =) (helpersN, helper_lines)
               |> nice_atp_problem readable_names
-    val conjecture_offset =
-      length fact_lines + length class_rel_lines + length arity_lines
-      + length helper_lines
   in
     (problem,
      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
-     conjecture_offset, fact_names)
+     offset_of_heading_in_problem conjsN problem 0,
+     fact_names |> Vector.fromList)
   end
 
 end;