# HG changeset patch
# User blanchet
# Date 1324382686 -3600
# Node ID ddbe94f7242c13b7763d270fd43768469d7ee0ea
# Parent  2cae3d86abe5e42bbdd670c4bc7668246718b9e6
ensure TPTP FOF/TFF/THF formulas are close

diff -r 2cae3d86abe5 -r ddbe94f7242c src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 20 10:42:33 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 20 13:04:46 2011 +0100
@@ -1563,8 +1563,8 @@
 fun atype_of_type_vars (Simple_Types (_, Polymorphic, _)) = SOME atype_of_types
   | atype_of_type_vars _ = NONE
 
-fun bound_tvars type_enc Ts =
-  mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts)
+fun bound_tvars type_enc sorts Ts =
+  (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
   #> mk_aquant AForall
         (map_filter (fn TVar (x as (s, _), _) =>
                         SOME ((make_schematic_type_var x, s),
@@ -1575,7 +1575,7 @@
   (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
    else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
   |> close_formula_universally
-  |> bound_tvars type_enc atomic_Ts
+  |> bound_tvars type_enc true atomic_Ts
 
 val type_tag = `(make_fixed_const NONE) type_tag_name
 
@@ -1889,7 +1889,7 @@
                             should_guard_var_in_formula
                             (if pos then SOME true else NONE)
    |> close_formula_universally
-   |> bound_tvars type_enc atomic_types,
+   |> bound_tvars type_enc true atomic_types,
    NONE,
    case locality of
      Intro => isabelle_info format introN
@@ -1930,7 +1930,7 @@
            |> formula_from_iformula ctxt format mono type_enc
                   should_guard_var_in_formula (SOME false)
            |> close_formula_universally
-           |> bound_tvars type_enc atomic_types, NONE, NONE)
+           |> bound_tvars type_enc true atomic_types, NONE, NONE)
 
 fun formula_line_for_free_type j phi =
   Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, NONE)
@@ -2127,7 +2127,7 @@
            |> formula_from_iformula ctxt format mono type_enc
                                     (K (K (K (K (K (K true)))))) (SOME true)
            |> close_formula_universally
-           |> bound_tvars type_enc (atomic_types_of T),
+           |> bound_tvars type_enc true (atomic_types_of T),
            isabelle_info format introN, NONE)
 
 fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
@@ -2205,7 +2205,7 @@
              |> formula_from_iformula ctxt format mono type_enc
                                       (K (K (K (K (K (K true)))))) (SOME true)
              |> close_formula_universally
-             |> n > 1 ? bound_tvars type_enc (atomic_types_of T)
+             |> bound_tvars type_enc (n > 1) (atomic_types_of T)
              |> maybe_negate,
              isabelle_info format introN, NONE)
   end