# HG changeset patch
# User blanchet
# Date 1304279612 -7200
# Node ID fa2cf11d63516bc77263577f9063e720d736a486
# Parent  f139d0ac2d448c31b95a225af70d270f88e1b959
beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)

diff -r f139d0ac2d44 -r fa2cf11d6351 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:57:45 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 21:53:32 2011 +0200
@@ -779,6 +779,8 @@
           if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T)
   end
 
+fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
+
 fun formula_line_for_sym_decl ctxt type_sys n s j (s', T_args, T, _, ary) =
   let
     val (arg_Ts, res_T) = n_ary_strip_type ary T
@@ -787,7 +789,8 @@
     val bound_tms =
       bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
     val bound_Ts =
-      arg_Ts |> map (if n > 1 then SOME else K NONE)
+      arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
+                             else NONE)
   in
     Formula (sym_decl_prefix ^ ascii_of s ^ "_" ^ string_of_int j, Axiom,
              CombConst ((s, s'), T, T_args)
@@ -807,11 +810,13 @@
       val decls =
         case decls of
           decl :: (decls' as _ :: _) =>
-          if forall (curry (op =) (result_type_of_decl decl)
-                     o result_type_of_decl) decls' then
-            [decl]
-          else
-            decls
+          let val T = result_type_of_decl decl in
+            if forall ((fn T' => Type.raw_instance (T', T))
+                       o result_type_of_decl) decls' then
+              [decl]
+            else
+              decls
+          end
         | _ => decls
       val n = length decls
       val decls =