# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID b9d7df8c51c8f8dfd7bd0918ed4dddab784edb80
# Parent  c9552e617accbec28ca31d761fcbe811cada4168
make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types

diff -r c9552e617acc -r b9d7df8c51c8 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
@@ -952,10 +952,15 @@
 
 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
 
-fun decl_line_for_sym s (s', _, T, pred_sym, ary, _) =
-  let val (arg_Ts, res_T) = chop_fun ary T in
-    Decl (sym_decl_prefix ^ s, (s, s'), map mangled_type_name arg_Ts,
-          if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T)
+fun decl_line_for_sym ctxt nonmono_Ts level s (s', _, T, pred_sym, ary, _) =
+  let
+    val translate_type =
+      mangled_type_name o homogenized_type ctxt nonmono_Ts level
+    val (arg_tys, res_ty) =
+      T |> chop_fun ary |>> map translate_type ||> translate_type
+  in
+    Decl (sym_decl_prefix ^ s, (s, s'), arg_tys,
+          if pred_sym then `I tptp_tff_bool_type else res_ty)
   end
 
 fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
@@ -991,7 +996,7 @@
 fun problem_lines_for_sym_decls ctxt conj_sym_kind nonmono_Ts type_sys
                                 (s, decls) =
   case type_sys of
-    Simple_Types _ => map (decl_line_for_sym s) decls
+    Simple_Types level => map (decl_line_for_sym ctxt nonmono_Ts level s) decls
   | _ =>
     let
       val decls =