1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Wed May 04 22:56:33 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed May 04 23:18:28 2011 +0200
     1.3 @@ -583,10 +583,14 @@
     1.4  Constants are annotated with their types, supplied as extra arguments, to
     1.5  resolve overloading.
     1.6  
     1.7 +\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with
     1.8 +its type using a function $\mathit{type\_info\/}(\tau, t)$.
     1.9 +
    1.10  \item[$\bullet$] \textbf{\textit{mono\_preds}:} Similar to \textit{preds}, but
    1.11 -the problem is additionally monomorphized. This corresponds to the traditional
    1.12 -encoding of types in an untyped logic without overloading (e.g., such as
    1.13 -performed by the ToFoF-E wrapper).
    1.14 +the problem is additionally monomorphized.
    1.15 +
    1.16 +\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
    1.17 +the problem is additionally monomorphized.
    1.18  
    1.19  \item[$\bullet$] \textbf{\textit{mangled\_preds}:} Similar to
    1.20  \textit{mono\_preds}, but types are mangled in constant names instead of being
    1.21 @@ -594,12 +598,6 @@
    1.22  $\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate
    1.23  $\mathit{has\_type\_}\tau(t)$.
    1.24  
    1.25 -\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with
    1.26 -its type using a function $\mathit{type\_info\/}(\tau, t)$.
    1.27 -
    1.28 -\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
    1.29 -the problem is additionally monomorphized.
    1.30 -
    1.31  \item[$\bullet$] \textbf{\textit{mangled\_tags}:} Similar to
    1.32  \textit{mono\_tags}, but types are mangled in constant names instead of being
    1.33  supplied as ground term arguments. The binary function

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed May 04 22:56:33 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed May 04 23:18:28 2011 +0200
     2.3 @@ -891,7 +891,6 @@
     2.4  fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab =
     2.5    let
     2.6      fun declare_sym decl decls =
     2.7 -      (* FIXME: use "insert_type" in all cases? *)
     2.8        case type_sys of
     2.9          Preds (Polymorphic, All_Types) => insert_type #3 decl decls
    2.10        | _ => insert (op =) decl decls
    2.11 @@ -918,12 +917,13 @@
    2.12                    ? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab)
    2.13                           facts
    2.14  
    2.15 -(* FIXME: use CombVar not CombConst for bound variables? *)
    2.16  fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
    2.17      String.isPrefix bound_var_prefix s
    2.18    | is_var_or_bound_var (CombVar _) = true
    2.19    | is_var_or_bound_var _ = false
    2.20  
    2.21 +(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
    2.22 +   out with monotonicity" paper presented at CADE 2011. *)
    2.23  fun add_combterm_nonmonotonic_types _ (SOME false) _ = I
    2.24    | add_combterm_nonmonotonic_types ctxt _
    2.25          (CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1),