# HG changeset patch
# User blanchet
# Date 1320574427 -3600
# Node ID d00339ae7fffb6f58029e2e02b58727299afec23
# Parent  68f3e073ee21e4f68790f3b86bf3a3c7f39b4aa1
repaired quantification over type variables for non-TFF1/THF encodings

diff -r 68f3e073ee21 -r d00339ae7fff src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Sat Nov 05 22:41:25 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Sun Nov 06 11:13:47 2011 +0100
@@ -1527,12 +1527,15 @@
    (("If", true), @{thms if_True if_False True_or_False})]
   |> map (apsnd (map zero_var_indexes))
 
+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)
   #> mk_aquant AForall
         (map_filter (fn TVar (x as (s, _), _) =>
                         SOME ((make_schematic_type_var x, s),
-                              SOME atype_of_types)
+                              atype_of_type_vars type_enc)
                       | _ => NONE) Ts)
 
 fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
@@ -1852,11 +1855,12 @@
   |> type_class_formula type_enc class
 
 fun formula_line_for_arity_clause format type_enc
-        ({name, prem_atoms, concl_atom, ...} : arity_clause) =
+        ({name, prem_atoms, concl_atom} : arity_clause) =
   Formula (arity_clause_prefix ^ name, Axiom,
            mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
                     (formula_from_arity_atom type_enc concl_atom)
-           |> close_formula_universally type_enc,
+           |> mk_aquant AForall
+                  (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
            isabelle_info format introN, NONE)
 
 fun formula_line_for_conjecture ctxt format mono type_enc