# HG changeset patch
# User blanchet
# Date 1304267845 -7200
# Node ID a8a80a2a34be4d078b5b5065e21eb412c528d5ce
# Parent  ad700c4f2471db85e9163a19ba9feb3c769ac2b8
merge symbol declarations that are type-instances of each other -- useful for type system "Args true" with monomorphization turned off

diff -r ad700c4f2471 -r a8a80a2a34be src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
@@ -753,21 +753,24 @@
 
 fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab =
   let
-    fun aux tm =
+    fun declare_sym (decl as (_, _, T, _, _)) decls =
+      if exists (curry Type.raw_instance T o #3) decls then decls
+      else decl :: filter_out ((fn T' => Type.raw_instance (T', T)) o #3) decls
+    fun do_term tm =
       let val (head, args) = strip_combterm_comb tm in
         (case head of
            CombConst ((s, s'), T, T_args) =>
            let val pred_sym = is_pred_sym repaired_sym_tab s in
              if should_declare_sym type_sys pred_sym s then
-               Symtab.insert_list (op =)
-                   (s, (s', T_args, T, pred_sym, length args))
+               Symtab.map_default (s, [])
+                   (declare_sym (s', T_args, T, pred_sym, length args))
              else
                I
            end
          | _ => I)
-        #> fold aux args
+        #> fold do_term args
       end
-  in aux end
+  in do_term end
 fun add_fact_syms_to_decl_table type_sys repaired_sym_tab =
   fact_lift (formula_fold
       (add_combterm_syms_to_decl_table type_sys repaired_sym_tab))