src/HOL/Tools/ATP/atp_translate.ML

       | 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
 
-fun add_term_vars type_enc =
-  let
-    fun vars bounds (ATerm (name as (s, _), tms)) =
-        (if is_tptp_variable s andalso
-            not (String.isPrefix tvar_prefix s) andalso
-            not (member (op =) bounds name) then
-           insert (op =) (name, NONE)
-         else
-           I)
-        #> fold (vars bounds) tms
-      | vars bounds (AAbs ((name, _), tm)) = vars (name :: bounds) tm
-  in vars end
-fun close_formula_universally type_enc =
-  close_universally (add_term_vars type_enc)
+fun add_term_vars bounds (ATerm (name as (s, _), tms)) =
+    (if is_tptp_variable s andalso
+        not (String.isPrefix tvar_prefix s) andalso
+        not (member (op =) bounds name) then
+       insert (op =) (name, NONE)
+     else
+       I)
+    #> fold (add_term_vars bounds) tms
+  | add_term_vars bounds (AAbs ((name, _), tm)) =
+    add_term_vars (name :: bounds) tm
+val close_formula_universally = close_universally add_term_vars
 
 fun add_iterm_vars bounds (IApp (tm1, tm2)) =
     fold (add_iterm_vars bounds) [tm1, tm2]
   | add_iterm_vars _ (IConst _) = I
   | add_iterm_vars bounds (IVar (name, T)) =

                       | _ => NONE) Ts)
 
 fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
   (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
    else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
-  |> close_formula_universally type_enc
+  |> close_formula_universally
   |> bound_tvars type_enc atomic_Ts
 
 val type_tag = `(make_fixed_const NONE) type_tag_name
 
 fun type_tag_idempotence_fact format type_enc =

   (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
    iformula
    |> formula_from_iformula ctxt format mono type_enc
                             should_guard_var_in_formula
                             (if pos then SOME true else NONE)
-   |> close_formula_universally type_enc
+   |> close_formula_universally
    |> bound_tvars type_enc atomic_types,
    NONE,
    case locality of
      Intro => isabelle_info format introN
    | Elim => isabelle_info format elimN

   let val ty_arg = ATerm (tvar_a_name, []) in
     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
              AConn (AImplies,
                     [type_class_formula type_enc subclass ty_arg,
                      type_class_formula type_enc superclass ty_arg])
-             |> close_formula_universally type_enc,
+             |> close_formula_universally,
              isabelle_info format introN, NONE)
   end
 
 fun formula_from_arity_atom type_enc (class, t, args) =
   ATerm (t, map (fn arg => ATerm (arg, [])) args)

         ({name, kind, iformula, atomic_types, ...} : translated_formula) =
   Formula (conjecture_prefix ^ name, kind,
            iformula
            |> formula_from_iformula ctxt format mono type_enc
                   should_guard_var_in_formula (SOME false)
-           |> close_formula_universally type_enc
+           |> close_formula_universally
            |> bound_tvars type_enc atomic_types, NONE, NONE)
 
 fun formula_line_for_free_type j phi =
   Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, NONE)
 fun formula_lines_for_free_types type_enc (facts : translated_formula list) =

            IConst (`make_bound_var "X", T, [])
            |> type_guard_iterm format type_enc T
            |> AAtom
            |> formula_from_iformula ctxt format mono type_enc
                                     (K (K (K (K (K (K true)))))) (SOME true)
-           |> close_formula_universally type_enc
+           |> close_formula_universally
            |> bound_tvars type_enc (atomic_types_of T),
            isabelle_info format introN, NONE)
 
 fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
   let val x_var = ATerm (`make_bound_var "X", []) in

              |> fold (curry (IApp o swap)) bounds
              |> type_guard_iterm format type_enc res_T
              |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
              |> formula_from_iformula ctxt format mono type_enc
                                       (K (K (K (K (K (K true)))))) (SOME true)
-             |> close_formula_universally type_enc
+             |> close_formula_universally
              |> n > 1 ? bound_tvars type_enc (atomic_types_of T)
              |> maybe_negate,
              isabelle_info format introN, NONE)
   end