1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
     1.3 @@ -753,21 +753,24 @@
     1.4  
     1.5  fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab =
     1.6    let
     1.7 -    fun aux tm =
     1.8 +    fun declare_sym (decl as (_, _, T, _, _)) decls =
     1.9 +      if exists (curry Type.raw_instance T o #3) decls then decls
    1.10 +      else decl :: filter_out ((fn T' => Type.raw_instance (T', T)) o #3) decls
    1.11 +    fun do_term tm =
    1.12        let val (head, args) = strip_combterm_comb tm in
    1.13          (case head of
    1.14             CombConst ((s, s'), T, T_args) =>
    1.15             let val pred_sym = is_pred_sym repaired_sym_tab s in
    1.16               if should_declare_sym type_sys pred_sym s then
    1.17 -               Symtab.insert_list (op =)
    1.18 -                   (s, (s', T_args, T, pred_sym, length args))
    1.19 +               Symtab.map_default (s, [])
    1.20 +                   (declare_sym (s', T_args, T, pred_sym, length args))
    1.21               else
    1.22                 I
    1.23             end
    1.24           | _ => I)
    1.25 -        #> fold aux args
    1.26 +        #> fold do_term args
    1.27        end
    1.28 -  in aux end
    1.29 +  in do_term end
    1.30  fun add_fact_syms_to_decl_table type_sys repaired_sym_tab =
    1.31    fact_lift (formula_fold
    1.32        (add_combterm_syms_to_decl_table type_sys repaired_sym_tab))