# HG changeset patch
# User blanchet
# Date 1323784542 -3600
# Node ID 45a5b6edd4f7b2d11de3b695e644c4dc2b808a11
# Parent  0b19934792d2c9083364f55836f3fb085f630053
added missing quantifier

diff -r 0b19934792d2 -r 45a5b6edd4f7 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 13 14:55:42 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 13 14:55:42 2011 +0100
@@ -1905,7 +1905,8 @@
              AConn (AImplies,
                     [type_class_formula type_enc subclass ty_arg,
                      type_class_formula type_enc superclass ty_arg])
-             |> close_formula_universally,
+             |> mk_aquant AForall
+                          [(tvar_a_name, atype_of_type_vars type_enc)],
              isabelle_info format introN, NONE)
   end