renamed type systems for more consistency

--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu May 12 11:03:48 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu May 12 15:29:18 2011 +0200
@@ -460,7 +460,7 @@
 developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
 servers. This ATP supports a fragment of the TPTP many-typed first-order format
 (TFF). It is supported primarily for experimenting with the
-\textit{type\_sys} $=$ \textit{simple} option (\S\ref{problem-encoding}).
+\textit{type\_sys} $=$ \textit{simple\_types} option (\S\ref{problem-encoding}).
 
 \item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
 developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
@@ -571,85 +571,81 @@
 following values:
 
 \begin{enum}
-\item[$\bullet$] \textbf{\textit{simple}:} Use the prover's support for
-many-typed first-order logic if available; otherwise, fall back on
-\textit{mangled\_preds}. The problem is monomorphized, meaning that the
-problem's type variables are instantiated with heuristically chosen ground
-types. Monomorphization can simplify reasoning but also leads to larger fact
-bases, which can slow down the ATPs.
+%\item[$\bullet$] \textbf{\textit{poly\_types}:} Use the prover's support for
+%polymorphic first-order logic if available; otherwise, fall back on
+%\textit{poly\_preds}.
 
-\item[$\bullet$] \textbf{\textit{preds}:} Types are encoded using a binary predicate
+\item[$\bullet$] \textbf{\textit{poly\_preds}:} Types are encoded using a predicate
 $\mathit{has\_type\/}(\tau, t)$ that restricts the range of bound variables.
 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
+\item[$\bullet$] \textbf{\textit{poly\_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.
+\item[$\bullet$] \textbf{\textit{poly\_args}:}
+Like for the other sound encodings, constants are annotated with their types to
+resolve overloading, but otherwise no type information is encoded.
 
-\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
-the problem is additionally monomorphized.
+\item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to
+the ATP. Types are simply erased.
 
-\item[$\bullet$] \textbf{\textit{mangled\_preds}:} Similar to
-\textit{mono\_preds}, but types are mangled in constant names instead of being
-supplied as ground term arguments. The binary predicate
-$\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate
-$\mathit{has\_type\_}\tau(t)$.
+\item[$\bullet$]
+\textbf{%
+\textit{mono\_preds},
+\textit{mono\_tags},
+\textit{mono\_args}:} \\
+Similar to \textit{poly\_preds}, \textit{poly\_tags}, and \textit{poly\_args},
+respectively, but the problem is additionally monomorphized, meaning that type
+variables are instantiated with heuristically chosen ground types.
+Monomorphization can simplify reasoning but also leads to larger fact bases,
+which can slow down the ATPs.
 
-\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
+\item[$\bullet$] \textbf{\textit{simple\_types}:} Use the prover's support for
+simply typed first-order logic if available; otherwise, fall back on
+\textit{mangled\_preds}. The problem is monomorphized.
+
+\item[$\bullet$]
+\textbf{%
+\textit{mangled\_preds},
+\textit{mangled\_tags},
+\textit{mangled\_args}:} \\
+Similar to
+\textit{mono\_preds}, \textit{mono\_tags}, and \textit{mono\_args},
+respectively but types are mangled in constant names instead of being supplied
+as ground term arguments. The binary predicate $\mathit{has\_type\/}(\tau, t)$
+becomes a unary predicate $\mathit{has\_type\_}\tau(t)$, and the binary function
 $\mathit{type\_info\/}(\tau, t)$ becomes a unary function
 $\mathit{type\_info\_}\tau(t)$.
 
 \item[$\bullet$]
 \textbf{%
-\textit{simple}?,
-\textit{preds}?,
-\textit{mono\_preds}?,
-\textit{mangled\_preds}?, \\
-\textit{tags}?,
-\textit{mono\_tags}?,
-\textit{mangled\_tags}?:} \\
-The type systems \textit{simple}, \textit{preds}, \textit{mono\_preds},
-\textit{mangled\_preds}, \textit{tags}, \textit{mono\_tags}, and
-\textit{mangled\_tags} are fully typed and virtually sound---i.e., except for
-pathological cases, all found proofs are type-correct. For each of these,
-Sledgehammer also provides a just-as-sound partially typed variant identified by
-a question mark (`{?}')\ that detects and erases monotonic types, notably infinite
-types. (For \textit{simple}, the types are not actually erased but rather
-replaced by a shared uniform ``top'' type.)
+\textit{simple\_types}?,
+\{\textit{poly},\textit{mono},\textit{mangled}\}\textit{\_}\{\textit{preds},\textit{tags}\}?:} \\
+The type systems \textit{poly\_preds}, \textit{poly\_tags},
+\textit{mono\_preds}, \textit{mono\_tags}, \textit{simple\_types},
+\textit{mangled\_preds}, and \textit{mangled\_tags} are fully typed and
+virtually sound---except for pathological cases, all found proofs are
+type-correct. For each of these, Sledgehammer also provides a just-as-sound
+partially typed variant identified by a question mark (`{?}')\ that detects and
+erases monotonic types, notably infinite types. (For \textit{simple\_types}, the
+types are not actually erased but rather replaced by a shared uniform type.)
 
 \item[$\bullet$]
 \textbf{%
-\textit{simple}!,
-\textit{preds}!,
-\textit{mono\_preds}!,
-\textit{mangled\_preds}!, \\
-\textit{tags}!,
-\textit{mono\_tags}!,
-\textit{mangled\_tags}!:} \\
+\textit{simple\_types}!,
+\{\textit{poly},\textit{mono},\textit{mangled}\}\textit{\_}\{\textit{preds},\textit{tags}\}!:} \\
 If the question mark (`{?}')\ is replaced by an exclamation mark (`{!}'),\ the
 translation erases all types except those that are clearly finite (e.g.,
 \textit{bool}). This encoding is unsound.
 
-\item[$\bullet$] \textbf{\textit{args}:}
-Like for the other sound encodings, constants are annotated with their types to
-resolve overloading, but otherwise no type information is encoded. This encoding
-is hence less sound than the exclamation mark (`{!}')\ variants described above.
-
-\item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to
-the ATP. Types are simply erased.
-
 \item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
 uses a fully typed, virtually sound encoding; otherwise, uses any encoding. The
 actual encoding used depends on the ATP and should be the most efficient for
 that ATP.
 \end{enum}
 
-For SMT solvers and ToFoF-E, the type system is always \textit{simple}.
+For SMT solvers and ToFoF-E, the type system is always \textit{simple\_types}.
 
 \opdefault{monomorphize\_limit}{int}{\upshape 4}
 Specifies the maximum number of iterations for the monomorphization fixpoint

--- a/src/HOL/Metis_Examples/HO_Reas.thy	Thu May 12 11:03:48 2011 +0200
+++ b/src/HOL/Metis_Examples/HO_Reas.thy	Thu May 12 15:29:18 2011 +0200
@@ -14,12 +14,12 @@
 
 lemma "id True"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = tags!, expect = some] (id_apply)
-sledgehammer [type_sys = tags?, expect = some] (id_apply)
-sledgehammer [type_sys = tags, expect = some] (id_apply)
-sledgehammer [type_sys = preds!, expect = some] (id_apply)
-sledgehammer [type_sys = preds?, expect = some] (id_apply)
-sledgehammer [type_sys = preds, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -27,12 +27,12 @@
 
 lemma "\<not> id False"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = tags!, expect = some] (id_apply)
-sledgehammer [type_sys = tags?, expect = some] (id_apply)
-sledgehammer [type_sys = tags, expect = some] (id_apply)
-sledgehammer [type_sys = preds!, expect = some] (id_apply)
-sledgehammer [type_sys = preds?, expect = some] (id_apply)
-sledgehammer [type_sys = preds, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -40,12 +40,12 @@
 
 lemma "x = id True \<or> x = id False"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = tags!, expect = some] (id_apply)
-sledgehammer [type_sys = tags?, expect = some] (id_apply)
-sledgehammer [type_sys = tags, expect = some] (id_apply)
-sledgehammer [type_sys = preds, expect = some] (id_apply)
-sledgehammer [type_sys = preds!, expect = some] (id_apply)
-sledgehammer [type_sys = preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -53,12 +53,12 @@
 
 lemma "id x = id True \<or> id x = id False"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = tags!, expect = some] (id_apply)
-sledgehammer [type_sys = tags?, expect = some] (id_apply)
-sledgehammer [type_sys = tags, expect = some] (id_apply)
-sledgehammer [type_sys = preds!, expect = some] (id_apply)
-sledgehammer [type_sys = preds?, expect = some] (id_apply)
-sledgehammer [type_sys = preds, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -66,13 +66,13 @@
 
 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
 sledgehammer [type_sys = erased, expect = none] ()
-sledgehammer [type_sys = args, expect = none] ()
-sledgehammer [type_sys = tags!, expect = some] ()
-sledgehammer [type_sys = tags?, expect = some] ()
-sledgehammer [type_sys = tags, expect = some] ()
-sledgehammer [type_sys = preds!, expect = some] ()
-sledgehammer [type_sys = preds?, expect = some] ()
-sledgehammer [type_sys = preds, expect = some] ()
+sledgehammer [type_sys = poly_args, expect = none] ()
+sledgehammer [type_sys = poly_tags!, expect = some] ()
+sledgehammer [type_sys = poly_tags?, expect = some] ()
+sledgehammer [type_sys = poly_tags, expect = some] ()
+sledgehammer [type_sys = poly_preds!, expect = some] ()
+sledgehammer [type_sys = poly_preds?, expect = some] ()
+sledgehammer [type_sys = poly_preds, expect = some] ()
 sledgehammer [type_sys = mangled_preds!, expect = some] ()
 sledgehammer [type_sys = mangled_preds?, expect = some] ()
 sledgehammer [type_sys = mangled_preds, expect = some] ()
@@ -80,12 +80,12 @@
 
 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = tags!, expect = some] (id_apply)
-sledgehammer [type_sys = tags?, expect = some] (id_apply)
-sledgehammer [type_sys = tags, expect = some] (id_apply)
-sledgehammer [type_sys = preds!, expect = some] (id_apply)
-sledgehammer [type_sys = preds?, expect = some] (id_apply)
-sledgehammer [type_sys = preds, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -93,12 +93,12 @@
 
 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = tags!, expect = some] (id_apply)
-sledgehammer [type_sys = tags?, expect = some] (id_apply)
-sledgehammer [type_sys = tags, expect = some] (id_apply)
-sledgehammer [type_sys = preds!, expect = some] (id_apply)
-sledgehammer [type_sys = preds?, expect = some] (id_apply)
-sledgehammer [type_sys = preds, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -106,12 +106,12 @@
 
 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = tags!, expect = some] (id_apply)
-sledgehammer [type_sys = tags?, expect = some] (id_apply)
-sledgehammer [type_sys = tags, expect = some] (id_apply)
-sledgehammer [type_sys = preds!, expect = some] (id_apply)
-sledgehammer [type_sys = preds?, expect = some] (id_apply)
-sledgehammer [type_sys = preds, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -119,12 +119,12 @@
 
 lemma "id (a \<and> b) \<Longrightarrow> id a"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = tags!, expect = some] (id_apply)
-sledgehammer [type_sys = tags?, expect = some] (id_apply)
-sledgehammer [type_sys = tags, expect = some] (id_apply)
-sledgehammer [type_sys = preds!, expect = some] (id_apply)
-sledgehammer [type_sys = preds?, expect = some] (id_apply)
-sledgehammer [type_sys = preds, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -132,12 +132,12 @@
 
 lemma "id (a \<and> b) \<Longrightarrow> id b"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = tags!, expect = some] (id_apply)
-sledgehammer [type_sys = tags?, expect = some] (id_apply)
-sledgehammer [type_sys = tags, expect = some] (id_apply)
-sledgehammer [type_sys = preds!, expect = some] (id_apply)
-sledgehammer [type_sys = preds?, expect = some] (id_apply)
-sledgehammer [type_sys = preds, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -145,12 +145,12 @@
 
 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = tags!, expect = some] (id_apply)
-sledgehammer [type_sys = tags?, expect = some] (id_apply)
-sledgehammer [type_sys = tags, expect = some] (id_apply)
-sledgehammer [type_sys = preds!, expect = some] (id_apply)
-sledgehammer [type_sys = preds?, expect = some] (id_apply)
-sledgehammer [type_sys = preds, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -158,12 +158,12 @@
 
 lemma "id a \<Longrightarrow> id (a \<or> b)"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = tags!, expect = some] (id_apply)
-sledgehammer [type_sys = tags?, expect = some] (id_apply)
-sledgehammer [type_sys = tags, expect = some] (id_apply)
-sledgehammer [type_sys = preds!, expect = some] (id_apply)
-sledgehammer [type_sys = preds?, expect = some] (id_apply)
-sledgehammer [type_sys = preds, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -171,12 +171,12 @@
 
 lemma "id b \<Longrightarrow> id (a \<or> b)"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = tags!, expect = some] (id_apply)
-sledgehammer [type_sys = tags?, expect = some] (id_apply)
-sledgehammer [type_sys = tags, expect = some] (id_apply)
-sledgehammer [type_sys = preds!, expect = some] (id_apply)
-sledgehammer [type_sys = preds?, expect = some] (id_apply)
-sledgehammer [type_sys = preds, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -184,12 +184,12 @@
 
 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = tags!, expect = some] (id_apply)
-sledgehammer [type_sys = tags?, expect = some] (id_apply)
-sledgehammer [type_sys = tags, expect = some] (id_apply)
-sledgehammer [type_sys = preds!, expect = some] (id_apply)
-sledgehammer [type_sys = preds?, expect = some] (id_apply)
-sledgehammer [type_sys = preds, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -197,12 +197,12 @@
 
 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = tags!, expect = some] (id_apply)
-sledgehammer [type_sys = tags?, expect = some] (id_apply)
-sledgehammer [type_sys = tags, expect = some] (id_apply)
-sledgehammer [type_sys = preds, expect = some] (id_apply)
-sledgehammer [type_sys = preds!, expect = some] (id_apply)
-sledgehammer [type_sys = preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -210,12 +210,12 @@
 
 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = tags!, expect = some] (id_apply)
-sledgehammer [type_sys = tags?, expect = some] (id_apply)
-sledgehammer [type_sys = tags, expect = some] (id_apply)
-sledgehammer [type_sys = preds!, expect = some] (id_apply)
-sledgehammer [type_sys = preds?, expect = some] (id_apply)
-sledgehammer [type_sys = preds, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu May 12 11:03:48 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu May 12 15:29:18 2011 +0200
@@ -23,6 +23,12 @@
                * string fo_term option * string fo_term option
   type 'a problem = (string * 'a problem_line list) list
 
+(* official TPTP syntax *)
+  val tptp_tff_type_of_types : string
+  val tptp_tff_bool_type : string
+  val tptp_tff_individual_type : string
+  val tptp_false : string
+  val tptp_true : string
   val timestamp : unit -> string
   val hashw : word * word -> word
   val hashw_string : string * word -> word
@@ -55,6 +61,13 @@
              * string fo_term option * string fo_term option
 type 'a problem = (string * 'a problem_line list) list
 
+(* official TPTP syntax *)
+val tptp_tff_type_of_types = "$tType"
+val tptp_tff_bool_type = "$o"
+val tptp_tff_individual_type = "$i"
+val tptp_false = "$false"
+val tptp_true = "$true"
+
 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
 
 (* This hash function is recommended in Compilers: Principles, Techniques, and
@@ -87,20 +100,21 @@
   | string_for_connective AIf = "<="
   | string_for_connective AIff = "<=>"
   | string_for_connective ANotIff = "<~>"
-fun string_for_bound_var (s, NONE) = s
-  | string_for_bound_var (s, SOME ty) = s ^ " : " ^ ty
-fun string_for_formula (AQuant (q, xs, phi)) =
+fun string_for_bound_var Fof (s, _) = s
+  | string_for_bound_var Tff (s, ty) =
+    s ^ " : " ^ (ty |> the_default tptp_tff_individual_type)
+fun string_for_formula format (AQuant (q, xs, phi)) =
     "(" ^ string_for_quantifier q ^
-    "[" ^ commas (map string_for_bound_var xs) ^ "] : " ^
-    string_for_formula phi ^ ")"
-  | string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
+    "[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^
+    string_for_formula format phi ^ ")"
+  | string_for_formula _ (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
     space_implode " != " (map string_for_term ts)
-  | string_for_formula (AConn (c, [phi])) =
-    "(" ^ string_for_connective c ^ " " ^ string_for_formula phi ^ ")"
-  | string_for_formula (AConn (c, phis)) =
+  | string_for_formula format (AConn (c, [phi])) =
+    "(" ^ string_for_connective c ^ " " ^ string_for_formula format phi ^ ")"
+  | string_for_formula format (AConn (c, phis)) =
     "(" ^ space_implode (" " ^ string_for_connective c ^ " ")
-                        (map string_for_formula phis) ^ ")"
-  | string_for_formula (AAtom tm) = string_for_term tm
+                        (map (string_for_formula format) phis) ^ ")"
+  | string_for_formula _ (AAtom tm) = string_for_term tm
 
 fun string_for_symbol_type [] res_ty = res_ty
   | string_for_symbol_type [arg_ty] res_ty = arg_ty ^ " > " ^ res_ty
@@ -117,7 +131,7 @@
                             (Formula (ident, kind, phi, source, useful_info)) =
     (case format of Fof => "fof" | Tff => "tff") ^
     "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
-    string_for_formula phi ^ ")" ^
+    string_for_formula format phi ^ ")" ^
     (case (source, useful_info) of
        (NONE, NONE) => ""
      | (SOME tm, NONE) => ", " ^ string_for_term tm

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 11:03:48 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:18 2011 +0200
@@ -18,7 +18,7 @@
     All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
 
   datatype type_system =
-    Simple of type_level |
+    Simple_Types of type_level |
     Preds of polymorphism * type_level |
     Tags of polymorphism * type_level
 
@@ -84,12 +84,6 @@
 
 fun make_tff_type s = tff_type_prefix ^ ascii_of s
 
-(* official TPTP syntax *)
-val tptp_tff_type_of_types = "$tType"
-val tptp_tff_bool_type = "$o"
-val tptp_false = "$false"
-val tptp_true = "$true"
-
 (* Freshness almost guaranteed! *)
 val sledgehammer_weak_prefix = "Sledgehammer:"
 
@@ -98,7 +92,7 @@
   All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
 
 datatype type_system =
-  Simple of type_level |
+  Simple_Types of type_level |
   Preds of polymorphism * type_level |
   Tags of polymorphism * type_level
 
@@ -106,12 +100,15 @@
   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
 
 fun type_sys_from_string s =
-  (case try (unprefix "mangled_") s of
-     SOME s => (Mangled_Monomorphic, s)
+  (case try (unprefix "poly_") s of
+     SOME s => (SOME Polymorphic, s)
    | NONE =>
      case try (unprefix "mono_") s of
-       SOME s => (Monomorphic, s)
-     | NONE => (Polymorphic, s))
+       SOME s => (SOME Monomorphic, s)
+     | NONE =>
+       case try (unprefix "mangled_") s of
+         SOME s => (SOME Mangled_Monomorphic, s)
+       | NONE => (NONE, s))
   ||> (fn s =>
           (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
           case try_unsuffixes ["?", "_query"] s of
@@ -120,22 +117,22 @@
             case try_unsuffixes ["!", "_bang"] s of
               SOME s => (Finite_Types, s)
             | NONE => (All_Types, s))
-  |> (fn (polymorphism, (level, core)) =>
-         case (core, (polymorphism, level)) of
-           ("simple", (Polymorphic (* naja *), level)) => Simple level
-         | ("preds", extra) => Preds extra
-         | ("tags", extra) => Tags extra
-         | ("args", (_, All_Types (* naja *))) =>
-           Preds (polymorphism, Const_Arg_Types)
-         | ("erased", (Polymorphic, All_Types (* naja *))) =>
-           Preds (polymorphism, No_Types)
+  |> (fn (poly, (level, core)) =>
+         case (core, (poly, level)) of
+           ("simple_types", (NONE, level)) => Simple_Types level
+         | ("preds", (SOME poly, level)) => Preds (poly, level)
+         | ("tags", (SOME poly, level)) => Tags (poly, level)
+         | ("args", (SOME poly, All_Types (* naja *))) =>
+           Preds (poly, Const_Arg_Types)
+         | ("erased", (NONE, All_Types (* naja *))) =>
+           Preds (Polymorphic, No_Types)
          | _ => error ("Unknown type system: " ^ quote s ^ "."))
 
-fun polymorphism_of_type_sys (Simple _) = Mangled_Monomorphic
+fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
   | polymorphism_of_type_sys (Preds (poly, _)) = poly
   | polymorphism_of_type_sys (Tags (poly, _)) = poly
 
-fun level_of_type_sys (Simple level) = level
+fun level_of_type_sys (Simple_Types level) = level
   | level_of_type_sys (Preds (_, level)) = level
   | level_of_type_sys (Tags (_, level)) = level
 
@@ -830,7 +827,7 @@
       end
     val do_bound_type =
       case type_sys of
-        Simple level =>
+        Simple_Types level =>
         SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level
       | _ => K NONE
     fun do_out_of_bound_type (s, T) =
@@ -933,7 +930,7 @@
 fun should_declare_sym type_sys pred_sym s =
   not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
   not (String.isPrefix "$" s) andalso
-  ((case type_sys of Simple _ => true | _ => false) orelse not pred_sym)
+  ((case type_sys of Simple_Types _ => true | _ => false) orelse not pred_sym)
 
 fun sym_decl_table_for_facts type_sys repaired_sym_tab (conjs, facts) =
   let
@@ -1029,7 +1026,7 @@
 fun problem_lines_for_sym_decls ctxt conj_sym_kind nonmono_Ts type_sys
                                 (s, decls) =
   case type_sys of
-    Simple _ => map (decl_line_for_sym s) decls
+    Simple_Types _ => map (decl_line_for_sym s) decls
   | _ =>
     let
       val decls =
@@ -1129,7 +1126,7 @@
     val problem =
       problem
       |> (case type_sys of
-            Simple _ =>
+            Simple_Types _ =>
             cons (type_declsN,
                   map decl_line_for_tff_type (tff_types_in_problem problem))
           | _ => I)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 11:03:48 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:18 2011 +0200
@@ -346,14 +346,12 @@
 val atp_important_message_keep_quotient = 10
 
 val fallback_best_type_systems =
-  [Preds (Polymorphic, Const_Arg_Types), Simple All_Types]
+  [Preds (Polymorphic, Const_Arg_Types), Simple_Types All_Types]
 
-fun adjust_dumb_type_sys formats (Simple level) =
-    if member (op =) formats Tff then (Tff, Simple level)
+fun adjust_dumb_type_sys formats (Simple_Types level) =
+    if member (op =) formats Tff then (Tff, Simple_Types level)
     else (Fof, Preds (Mangled_Monomorphic, level))
-  | adjust_dumb_type_sys formats type_sys =
-    if member (op =) formats Fof then (Fof, type_sys)
-    else (Tff, Simple (level_of_type_sys type_sys))
+  | adjust_dumb_type_sys formats type_sys = (hd formats, type_sys)
 fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
     adjust_dumb_type_sys formats type_sys
   | determine_format_and_type_sys best_type_systems formats