# HG changeset patch
# User blanchet
# Date 1341956163 -7200
# Node ID c9454e43466592afac8de6cf7e2d0263fd49557e
# Parent  d7ad89f6076824a3bbd71ac91b6eb2e9f1b4ae74
tuning

diff -r d7ad89f60768 -r c9454e434665 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jul 10 23:36:03 2012 +0200
@@ -2496,8 +2496,7 @@
   let
     val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
     val mono_lines = lines_for_mono_types ctxt mono type_enc mono_Ts
-    val decl_lines =
-      fold_rev (append o lines_for_sym_decls ctxt mono type_enc) syms []
+    val decl_lines = maps (lines_for_sym_decls ctxt mono type_enc) syms
   in mono_lines @ decl_lines end
 
 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
diff -r d7ad89f60768 -r c9454e434665 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Jul 10 23:36:03 2012 +0200
@@ -131,7 +131,7 @@
 fun type_instance thy T T' = Sign.typ_instance thy (T, T')
 fun type_generalization thy T T' = Sign.typ_instance thy (T', T)
 fun type_intersect thy T T' =
-  can (Sign.typ_unify thy (T, Logic.incr_tvar (maxidx_of_typ T + 1) T'))
+  can (Sign.typ_unify thy (Logic.incr_tvar (maxidx_of_typ T' + 1) T, T'))
       (Vartab.empty, 0)
 val type_equiv = Sign.typ_equiv