# HG changeset patch
# User blanchet
# Date 1304543908 -7200
# Node ID 7a5116bd63b75ed4a566a9ac04c0ed9f744f2618
# Parent  2123b2608b14def059da993d63dc6c5ee7433bce
documentation tuning

diff -r 2123b2608b14 -r 7a5116bd63b7 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Wed May 04 22:56:33 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed May 04 23:18:28 2011 +0200
@@ -583,10 +583,14 @@
 Constants are annotated with their types, supplied as extra arguments, to
 resolve overloading.
 
+\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with
+its type using a function $\mathit{type\_info\/}(\tau, t)$.
+
 \item[$\bullet$] \textbf{\textit{mono\_preds}:} Similar to \textit{preds}, but
-the problem is additionally monomorphized. This corresponds to the traditional
-encoding of types in an untyped logic without overloading (e.g., such as
-performed by the ToFoF-E wrapper).
+the problem is additionally monomorphized.
+
+\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
+the problem is additionally monomorphized.
 
 \item[$\bullet$] \textbf{\textit{mangled\_preds}:} Similar to
 \textit{mono\_preds}, but types are mangled in constant names instead of being
@@ -594,12 +598,6 @@
 $\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate
 $\mathit{has\_type\_}\tau(t)$.
 
-\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with
-its type using a function $\mathit{type\_info\/}(\tau, t)$.
-
-\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
-the problem is additionally monomorphized.
-
 \item[$\bullet$] \textbf{\textit{mangled\_tags}:} Similar to
 \textit{mono\_tags}, but types are mangled in constant names instead of being
 supplied as ground term arguments. The binary function
diff -r 2123b2608b14 -r 7a5116bd63b7 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed May 04 22:56:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed May 04 23:18:28 2011 +0200
@@ -891,7 +891,6 @@
 fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab =
   let
     fun declare_sym decl decls =
-      (* FIXME: use "insert_type" in all cases? *)
       case type_sys of
         Preds (Polymorphic, All_Types) => insert_type #3 decl decls
       | _ => insert (op =) decl decls
@@ -918,12 +917,13 @@
                   ? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab)
                          facts
 
-(* FIXME: use CombVar not CombConst for bound variables? *)
 fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
     String.isPrefix bound_var_prefix s
   | is_var_or_bound_var (CombVar _) = true
   | is_var_or_bound_var _ = false
 
+(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
+   out with monotonicity" paper presented at CADE 2011. *)
 fun add_combterm_nonmonotonic_types _ (SOME false) _ = I
   | add_combterm_nonmonotonic_types ctxt _
         (CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1),