# HG changeset patch
# User blanchet
# Date 1357231236 -3600
# Node ID 573d84e08f3f9756ea68562dd16fcfb866d0692c
# Parent  0e943b33d907ff896b121d1525e5545215cb5ecb
close formulas in the natural order, not its reverse -- so that Skolem arguments appear in the right order in Isar proofs

diff -r 0e943b33d907 -r 573d84e08f3f src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jan 03 17:28:55 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jan 03 17:40:36 2013 +0100
@@ -1027,7 +1027,7 @@
       | add_formula_vars bounds (AConn (_, phis)) =
         fold (add_formula_vars bounds) phis
       | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
-  in mk_aquant AForall (add_formula_vars [] phi []) phi end
+  in mk_aquant AForall (rev (add_formula_vars [] phi [])) phi end
 
 fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
     (if is_tptp_variable s andalso
@@ -1039,6 +1039,7 @@
     #> fold (add_term_vars bounds) tms
   | add_term_vars bounds (AAbs (((name, _), tm), args)) =
     add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args
+
 fun close_formula_universally phi = close_universally add_term_vars phi
 
 fun add_iterm_vars bounds (IApp (tm1, tm2)) =
@@ -1277,7 +1278,7 @@
   handle TERM _ => @{const True}
 
 (* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "="
-   for obscure technical reasons. *)
+   for technical reasons. *)
 fun should_use_iff_for_eq CNF _ = false
   | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format)
   | should_use_iff_for_eq _ _ = true