# HG changeset patch
# User blanchet
# Date 1328192058 -3600
# Node ID ef8d65f64f777e8a8d8b55e2bcb2801d3926ea5a
# Parent  cbc398fb30bb78db4fa2e99558719e5555f2a726
change 9ce354a77908 wasn't quite right -- here's an improvement

diff -r cbc398fb30bb -r ef8d65f64f77 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Feb 02 12:51:03 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Feb 02 15:14:18 2012 +0100
@@ -2386,7 +2386,7 @@
 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
 
 fun do_app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono
-        type_enc sym_tab base_s0 types in_conj =
+        type_enc sym_tab0 sym_tab base_s0 types in_conj =
   let
     fun do_alias ary =
       let
@@ -2397,7 +2397,7 @@
         val T_args = robust_const_typargs thy (base_s0, T)
         val (base_name as (base_s, _), T_args) =
           mangle_type_args_in_const format type_enc base_name T_args
-        val base_ary = min_ary_of sym_tab base_s
+        val base_ary = min_ary_of sym_tab0 base_s
         val T_args =
           T_args |> filter_type_args_in_const thy monom_constrs type_enc
                                               base_ary base_s
@@ -2430,7 +2430,8 @@
       end
   in do_alias end
 fun app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono
-        type_enc sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) =
+                               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 app_op_alias_sep mangled_s then
@@ -2438,18 +2439,19 @@
         val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
       in
         do_app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
-            mono type_enc sym_tab base_s0 types in_conj min_ary
+            mono type_enc sym_tab0 sym_tab base_s0 types in_conj min_ary
       end
     else
       ([], [])
   | NONE => ([], [])
 fun app_op_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind
-                                     mono type_enc app_op_aliases sym_tab =
+        mono type_enc app_op_aliases sym_tab0 sym_tab =
   ([], [])
   |> app_op_aliases
-     ? Symtab.fold_rev (pair_append
-                        o app_op_alias_lines_for_sym ctxt monom_constrs format
-                              conj_sym_kind mono type_enc sym_tab) sym_tab 
+     ? Symtab.fold_rev
+           (pair_append
+            o app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
+                  mono type_enc sym_tab0 sym_tab) sym_tab
 
 fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
     Config.get ctxt type_tag_idempotence andalso
@@ -2570,13 +2572,13 @@
          lifted) =
       translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts
                          concl_t facts
-    val sym_tab = sym_table_for_facts ctxt type_enc app_op_level conjs facts
+    val sym_tab0 = sym_table_for_facts ctxt type_enc app_op_level conjs facts
     val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
     val (polym_constrs, monom_constrs) =
       all_constrs_of_polymorphic_datatypes thy
       |>> map (make_fixed_const (SOME format))
     fun firstorderize in_helper =
-      firstorderize_fact thy monom_constrs format type_enc sym_tab
+      firstorderize_fact thy monom_constrs format type_enc sym_tab0
                          (app_op_aliases andalso not in_helper)
     val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
     val sym_tab = sym_table_for_facts ctxt type_enc Incomplete_Apply conjs facts
@@ -2588,7 +2590,7 @@
     val class_decl_lines = decl_lines_for_classes type_enc classes
     val (app_op_alias_eq_tms, app_op_alias_eq_lines) =
       app_op_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind
-                                       mono type_enc app_op_aliases sym_tab
+          mono type_enc app_op_aliases sym_tab0 sym_tab
     val sym_decl_lines =
       (conjs, helpers @ facts, app_op_alias_eq_tms)
       |> sym_decl_table_for_facts ctxt format type_enc sym_tab
diff -r cbc398fb30bb -r ef8d65f64f77 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Feb 02 12:51:03 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Feb 02 15:14:18 2012 +0100
@@ -355,7 +355,8 @@
    required_execs =
      [("SPASS_NEW_HOME", "SPASS"), ("SPASS_NEW_HOME", "tptp2dfg")],
    arguments = fn _ => fn _ => fn incomplete => fn timeout => fn _ =>
-     ("-Auto -LR=1 -Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
+     ("-Auto -LR=1 -LT=1 -Isabelle=1 -TimeLimit=" ^
+      string_of_int (to_secs 1 timeout))
      |> incomplete = spass_incompleteN ? prefix "-Splits=0 -FullRed=0 ",
    proof_delims = #proof_delims spass_config,
    known_failures = #known_failures spass_config,