merged

--- a/src/HOL/TPTP/atp_theory_export.ML	Mon Apr 08 14:18:39 2013 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Mon Apr 08 14:28:37 2013 +0200
@@ -114,11 +114,14 @@
     handle TYPE _ => @{prop True}
   end
 
+fun heading_sort_key heading =
+  if String.isPrefix "Relevant fact" heading then "_" ^ heading else heading
+
 fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
   let
     val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val type_enc =
-      type_enc |> type_enc_from_string Strict
+      type_enc |> type_enc_from_string Non_Strict
                |> adjust_type_enc format
     val mono = not (is_type_enc_polymorphic type_enc)
     val path = file_name |> Path.explode
@@ -126,6 +129,7 @@
     val facts =
       Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false
                                   Symtab.empty [] [] css_table
+      |> sort (Sledgehammer_MaSh.crude_thm_ord o pairself snd)
     val atp_problem =
       facts
       |> map (fn ((_, loc), th) =>
@@ -137,6 +141,7 @@
     val atp_problem =
       atp_problem
       |> map (apsnd (filter_out (is_problem_line_tautology ctxt format)))
+      |> sort_wrt (heading_sort_key o fst)
     val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts
     val infers =
       facts
@@ -155,6 +160,9 @@
       |> fold (fn (to, froms) =>
                   fold (fn from => String_Graph.add_edge (from, to)) froms)
               infers
+      |> fold (fn (to, from) => String_Graph.add_edge_acyclic (from, to))
+              (tl all_atp_problem_names
+               ~~ fst (split_last all_atp_problem_names))
       |> String_Graph.topological_order
     val order_tab =
       Symtab.empty

--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Apr 08 14:18:39 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Apr 08 14:28:37 2013 +0200
@@ -267,9 +267,7 @@
   |> Real.ceil |> signed_string_of_int
 
 fun e_selection_weight_arguments ctxt heuristic sel_weights =
-  if heuristic = e_autoN then
-    "-xAuto"
-  else
+  if heuristic = e_fun_weightN orelse heuristic = e_sym_offset_weightN then
     (* supplied by Stephan Schulz *)
     "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
     \--destructive-er-aggressive --destructive-er --presat-simplify \
@@ -288,6 +286,8 @@
     "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
     \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
     \FIFOWeight(PreferProcessed))'"
+  else
+    "-xAuto"
 
 val e_ord_weights =
   map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","