--- 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)
--- 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