# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID f365f5138771ce329682add941c8bfe73ed71e1b
# Parent  70fc448a18153898c1f6dc5f2fad824a6815915c
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)

diff -r 70fc448a1815 -r f365f5138771 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Thu May 12 15:29:18 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Thu May 12 15:29:19 2011 +0200
@@ -67,6 +67,7 @@
     theory -> string list -> class list -> class list * arity_clause list
   val combtyp_of : combterm -> typ
   val strip_combterm_comb : combterm -> combterm * combterm list
+  val atyps_of : typ -> typ list
   val combterm_from_term :
     theory -> (string * typ) list -> term -> combterm * typ list
   val reveal_old_skolem_terms : (string * term) list -> term -> term
diff -r 70fc448a1815 -r f365f5138771 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:18 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
@@ -849,12 +849,16 @@
       | do_formula (AAtom tm) = AAtom (do_term true tm)
   in do_formula end
 
+fun bound_atomic_types type_sys Ts =
+  mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
+                (atp_type_literals_for_types type_sys Axiom Ts))
+
 fun formula_for_fact ctxt nonmono_Ts type_sys
                      ({combformula, atomic_types, ...} : translated_formula) =
-  mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
-                (atp_type_literals_for_types type_sys Axiom atomic_types))
-           (formula_from_combformula ctxt nonmono_Ts type_sys
-                (close_combformula_universally combformula))
+  combformula
+  |> close_combformula_universally
+  |> formula_from_combformula ctxt nonmono_Ts type_sys
+  |> bound_atomic_types type_sys atomic_types
   |> close_formula_universally
 
 fun useful_isabelle_info s = SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
@@ -1019,6 +1023,7 @@
              |> type_pred_combatom ctxt nonmono_Ts type_sys res_T
              |> mk_aquant AForall (bound_names ~~ bound_Ts)
              |> formula_from_combformula ctxt nonmono_Ts type_sys
+             |> n > 1 ? bound_atomic_types type_sys (atyps_of T)
              |> close_formula_universally
              |> maybe_negate,
              NONE, NONE)