# HG changeset patch
# User huffman
# Date 1314307598 25200
# Node ID abcf7c0743e8a6704c1c2eeb83768200bdef68dd
# Parent  fbb777aec0d4ea16dbd43b09a5f909cf89889f1b# Parent  a4cbf5668a549034f470549df9f18969297d5a61
merged

diff -r fbb777aec0d4 -r abcf7c0743e8 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Aug 25 14:25:19 2011 -0700
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Aug 25 14:26:38 2011 -0700
@@ -896,7 +896,7 @@
 arguments, to resolve overloading.
 
 \item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
-tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$.
+tagged with its type using a function $\mathit{type\/}(\tau, t)$.
 
 \item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}
 Like for \textit{poly\_guards} constants are annotated with their types to
@@ -905,8 +905,8 @@
 
 \item[$\bullet$]
 \textbf{%
-\textit{mono\_guards}, \textit{mono\_tags} (sound);
-\textit{mono\_args} (unsound):} \\
+\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\
+\textit{raw\_mono\_args} (unsound):} \\
 Similar to \textit{poly\_guards}, \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.
@@ -915,33 +915,34 @@
 
 \item[$\bullet$]
 \textbf{%
-\textit{mangled\_guards},
-\textit{mangled\_tags} (sound); \\
-\textit{mangled\_args} (unsound):} \\
+\textit{mono\_guards}, \textit{mono\_tags} (sound);
+\textit{mono\_args} (unsound):} \\
 Similar to
-\textit{mono\_guards}, \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)$.
+\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and
+\textit{raw\_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\/}(\tau, t)$ becomes a unary function
+$\mathit{type\_}\tau(t)$.
 
 \item[$\bullet$] \textbf{\textit{simple} (sound):} Exploit simple first-order
 types if the prover supports the TFF or THF syntax; otherwise, fall back on
-\textit{mangled\_guards}. The problem is monomorphized.
+\textit{mono\_guards}. The problem is monomorphized.
 
 \item[$\bullet$] \textbf{\textit{simple\_higher} (sound):} Exploit simple
 higher-order types if the prover supports the THF syntax; otherwise, fall back
-on \textit{simple} or \textit{mangled\_guards\_uniform}. The problem is
+on \textit{simple} or \textit{mono\_guards\_uniform}. The problem is
 monomorphized.
 
 \item[$\bullet$]
 \textbf{%
-\textit{poly\_guards}?, \textit{poly\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
-\textit{mangled\_guards}?, \textit{mangled\_tags}?, \textit{simple}? (quasi-sound):} \\
+\textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\
+\textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
+\textit{simple}? (quasi-sound):} \\
 The type encodings \textit{poly\_guards}, \textit{poly\_tags},
-\textit{mono\_guards}, \textit{mono\_tags}, \textit{mangled\_guards},
-\textit{mangled\_tags}, and \textit{simple} are fully
+\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
+\textit{mono\_tags}, and \textit{simple} are fully
 typed and sound. For each of these, Sledgehammer also provides a lighter,
 virtually sound variant identified by a question mark (`{?}')\ that detects and
 erases monotonic types, notably infinite types. (For \textit{simple}, the types
@@ -952,12 +953,12 @@
 
 \item[$\bullet$]
 \textbf{%
-\textit{poly\_guards}!, \textit{poly\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
-\textit{mangled\_guards}!, \textit{mangled\_tags}!, \textit{simple}!, \textit{simple\_higher}! \\
-(mildly unsound):} \\
+\textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\
+\textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \textit{simple}!, \\
+\textit{simple\_higher}! (mildly unsound):} \\
 The type encodings \textit{poly\_guards}, \textit{poly\_tags},
-\textit{mono\_guards}, \textit{mono\_tags}, \textit{mangled\_guards},
-\textit{mangled\_tags}, \textit{simple}, and \textit{simple\_higher} also admit
+\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
+\textit{mono\_tags}, \textit{simple}, and \textit{simple\_higher} also admit
 a mildly unsound (but very efficient) variant identified by an exclamation mark
 (`{!}') that detects and erases erases all types except those that are clearly
 finite (e.g., \textit{bool}). (For \textit{simple} and \textit{simple\_higher},
@@ -973,7 +974,7 @@
 available in two variants, a ``uniform'' and a ``nonuniform'' variant. The
 nonuniform variants are generally more efficient and are the default; the
 uniform variants are identified by the suffix \textit{\_uniform} (e.g.,
-\textit{mangled\_guards\_uniform}{?}).
+\textit{mono\_guards\_uniform}{?}).
 
 For SMT solvers, the type encoding is always \textit{simple}, irrespective of
 the value of this option.
diff -r fbb777aec0d4 -r abcf7c0743e8 src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy	Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Metis_Examples/Proxies.thy	Thu Aug 25 14:26:38 2011 -0700
@@ -62,10 +62,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis (full_types) id_apply)
 
 lemma "id True"
@@ -74,10 +74,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "\<not> id False"
@@ -86,10 +86,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "x = id True \<or> x = id False"
@@ -98,10 +98,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id x = id True \<or> id x = id False"
@@ -110,10 +110,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
@@ -123,10 +123,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] ()
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] ()
-sledgehammer [type_enc = mangled_tags?, expect = some] ()
-sledgehammer [type_enc = mangled_tags, expect = some] ()
-sledgehammer [type_enc = mangled_guards?, expect = some] ()
-sledgehammer [type_enc = mangled_guards, expect = some] ()
+sledgehammer [type_enc = mono_tags?, expect = some] ()
+sledgehammer [type_enc = mono_tags, expect = some] ()
+sledgehammer [type_enc = mono_guards?, expect = some] ()
+sledgehammer [type_enc = mono_guards, expect = some] ()
 by (metis (full_types))
 
 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
@@ -135,10 +135,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
@@ -147,10 +147,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
@@ -159,10 +159,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (a \<and> b) \<Longrightarrow> id a"
@@ -171,10 +171,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (a \<and> b) \<Longrightarrow> id b"
@@ -183,10 +183,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
@@ -195,10 +195,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id a \<Longrightarrow> id (a \<or> b)"
@@ -207,10 +207,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id b \<Longrightarrow> id (a \<or> b)"
@@ -219,10 +219,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
@@ -231,10 +231,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
@@ -243,10 +243,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
@@ -255,10 +255,10 @@
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 end
diff -r fbb777aec0d4 -r abcf7c0743e8 src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Thu Aug 25 14:26:38 2011 -0700
@@ -29,42 +29,42 @@
    "poly_tags",
    "poly_tags_uniform",
    "poly_args",
+   "raw_mono_guards",
+   "raw_mono_guards_uniform",
+   "raw_mono_tags",
+   "raw_mono_tags_uniform",
+   "raw_mono_args",
    "mono_guards",
    "mono_guards_uniform",
    "mono_tags",
    "mono_tags_uniform",
    "mono_args",
-   "mangled_guards",
-   "mangled_guards_uniform",
-   "mangled_tags",
-   "mangled_tags_uniform",
-   "mangled_args",
    "simple",
    "poly_guards?",
    "poly_guards_uniform?",
    "poly_tags?",
    "poly_tags_uniform?",
+   "raw_mono_guards?",
+   "raw_mono_guards_uniform?",
+   "raw_mono_tags?",
+   "raw_mono_tags_uniform?",
    "mono_guards?",
    "mono_guards_uniform?",
    "mono_tags?",
    "mono_tags_uniform?",
-   "mangled_guards?",
-   "mangled_guards_uniform?",
-   "mangled_tags?",
-   "mangled_tags_uniform?",
    "simple?",
    "poly_guards!",
    "poly_guards_uniform!",
    "poly_tags!",
    "poly_tags_uniform!",
+   "raw_mono_guards!",
+   "raw_mono_guards_uniform!",
+   "raw_mono_tags!",
+   "raw_mono_tags_uniform!",
    "mono_guards!",
    "mono_guards_uniform!",
    "mono_tags!",
    "mono_tags_uniform!",
-   "mangled_guards!",
-   "mangled_guards_uniform!",
-   "mangled_tags!",
-   "mangled_tags_uniform!",
    "simple!"]
 
 fun metis_exhaust_tac ctxt ths =
diff -r fbb777aec0d4 -r abcf7c0743e8 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Aug 25 14:26:38 2011 -0700
@@ -484,9 +484,8 @@
     case result of
       SH_OK (time_isa, time_prover, names) =>
         let
-          fun get_thms (_, ATP_Translate.Chained) = NONE
-            | get_thms (name, loc) =
-              SOME ((name, loc), thms_of_name (Proof.context_of st) name)
+          fun get_thms (name, loc) =
+            SOME ((name, loc), thms_of_name (Proof.context_of st) name)
         in
           change_data id inc_sh_success;
           if trivial then () else change_data id inc_sh_nontriv_success;
diff -r fbb777aec0d4 -r abcf7c0743e8 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/SMT.thy	Thu Aug 25 14:26:38 2011 -0700
@@ -329,9 +329,24 @@
   if_True if_False not_not
 
 lemma [z3_rule]:
+  "(P \<and> Q) = (\<not>(\<not>P \<or> \<not>Q))"
+  "(P \<and> Q) = (\<not>(\<not>Q \<or> \<not>P))"
+  "(\<not>P \<and> Q) = (\<not>(P \<or> \<not>Q))"
+  "(\<not>P \<and> Q) = (\<not>(\<not>Q \<or> P))"
+  "(P \<and> \<not>Q) = (\<not>(\<not>P \<or> Q))"
+  "(P \<and> \<not>Q) = (\<not>(Q \<or> \<not>P))"
+  "(\<not>P \<and> \<not>Q) = (\<not>(P \<or> Q))"
+  "(\<not>P \<and> \<not>Q) = (\<not>(Q \<or> P))"
+  by auto
+
+lemma [z3_rule]:
   "(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
   "(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
   "(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
+  "(True \<longrightarrow> P) = P"
+  "(P \<longrightarrow> True) = True"
+  "(False \<longrightarrow> P) = True"
+  "(P \<longrightarrow> P) = True"
   by auto
 
 lemma [z3_rule]:
@@ -339,8 +354,18 @@
   by auto
 
 lemma [z3_rule]:
+  "(\<not>True) = False"
+  "(\<not>False) = True"
+  "(x = x) = True"
+  "(P = True) = P"
+  "(True = P) = P"
+  "(P = False) = (\<not>P)"
+  "(False = P) = (\<not>P)"
   "((\<not>P) = P) = False"
   "(P = (\<not>P)) = False"
+  "((\<not>P) = (\<not>Q)) = (P = Q)"
+  "\<not>(P = (\<not>Q)) = (P = Q)"
+  "\<not>((\<not>P) = Q) = (P = Q)"
   "(P \<noteq> Q) = (Q = (\<not>P))"
   "(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
   "(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
@@ -351,11 +376,36 @@
   "(if \<not>P then \<not>P else P) = True"
   "(if P then True else False) = P"
   "(if P then False else True) = (\<not>P)"
+  "(if P then Q else True) = ((\<not>P) \<or> Q)"
+  "(if P then Q else True) = (Q \<or> (\<not>P))"
+  "(if P then Q else \<not>Q) = (P = Q)"
+  "(if P then Q else \<not>Q) = (Q = P)"
+  "(if P then \<not>Q else Q) = (P = (\<not>Q))"
+  "(if P then \<not>Q else Q) = ((\<not>Q) = P)"
   "(if \<not>P then x else y) = (if P then y else x)"
+  "(if P then (if Q then x else y) else x) = (if P \<and> (\<not>Q) then y else x)"
+  "(if P then (if Q then x else y) else x) = (if (\<not>Q) \<and> P then y else x)"
+  "(if P then (if Q then x else y) else y) = (if P \<and> Q then x else y)"
+  "(if P then (if Q then x else y) else y) = (if Q \<and> P then x else y)"
+  "(if P then x else if P then y else z) = (if P then x else z)"
+  "(if P then x else if Q then x else y) = (if P \<or> Q then x else y)"
+  "(if P then x else if Q then x else y) = (if Q \<or> P then x else y)"
+  "(if P then x = y else x = z) = (x = (if P then y else z))"
+  "(if P then x = y else y = z) = (y = (if P then x else z))"
+  "(if P then x = y else z = y) = (y = (if P then x else z))"
   "f (if P then x else y) = (if P then f x else f y)"
   by auto
 
 lemma [z3_rule]:
+  "0 + (x::int) = x"
+  "x + 0 = x"
+  "x + x = 2 * x"
+  "0 * x = 0"
+  "1 * x = x"
+  "x + y = y + x"
+  by auto
+
+lemma [z3_rule]:  (* for def-axiom *)
   "P = Q \<or> P \<or> Q"
   "P = Q \<or> \<not>P \<or> \<not>Q"
   "(\<not>P) = Q \<or> \<not>P \<or> Q"
@@ -370,14 +420,18 @@
   "P \<or> Q \<or> (\<not>P) \<noteq> Q"
   "P \<or> \<not>Q \<or> P \<noteq> Q"
   "\<not>P \<or> Q \<or> P \<noteq> Q"
-  by auto
-
-lemma [z3_rule]:
-  "0 + (x::int) = x"
-  "x + 0 = x"
-  "0 * x = 0"
-  "1 * x = x"
-  "x + y = y + x"
+  "P \<or> y = (if P then x else y)"
+  "P \<or> (if P then x else y) = y"
+  "\<not>P \<or> x = (if P then x else y)"
+  "\<not>P \<or>  (if P then x else y) = x"
+  "P \<or> R \<or> \<not>(if P then Q else R)"
+  "\<not>P \<or> Q \<or> \<not>(if P then Q else R)"
+  "\<not>(if P then Q else R) \<or> \<not>P \<or> Q"
+  "\<not>(if P then Q else R) \<or> P \<or> R"
+  "(if P then Q else R) \<or> \<not>P \<or> \<not>Q"
+  "(if P then Q else R) \<or> P \<or> \<not>R"
+  "(if P then \<not>Q else R) \<or> \<not>P \<or> Q"
+  "(if P then Q else \<not>R) \<or> P \<or> R"
   by auto
 
 
diff -r fbb777aec0d4 -r abcf7c0743e8 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Set.thy	Thu Aug 25 14:26:38 2011 -0700
@@ -1378,6 +1378,9 @@
 lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
   by (fact compl_eq_compl_iff)
 
+lemma Compl_insert: "- insert x A = (-A) - {x}"
+  by blast
+
 text {* \medskip Bounded quantifiers.
 
   The following are not added to the default simpset because
diff -r fbb777aec0d4 -r abcf7c0743e8 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 25 14:26:38 2011 -0700
@@ -50,6 +50,7 @@
   val tptp_ho_forall : string
   val tptp_exists : string
   val tptp_ho_exists : string
+  val tptp_choice : string
   val tptp_not : string
   val tptp_and : string
   val tptp_or : string
@@ -147,6 +148,7 @@
 val tptp_ho_forall = "!!"
 val tptp_exists = "?"
 val tptp_ho_exists = "??"
+val tptp_choice = "@+"
 val tptp_not = "~"
 val tptp_and = "&"
 val tptp_or = "|"
@@ -264,13 +266,21 @@
       space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
       |> is_format_thf format ? enclose "(" ")"
     else
-      (case (s = tptp_ho_forall orelse s = tptp_ho_exists, ts) of
-         (true, [AAbs ((s', ty), tm)]) =>
+      (case (s = tptp_ho_forall orelse s = tptp_ho_exists,
+             s = tptp_choice andalso format = THF With_Choice, ts) of
+         (true, _, [AAbs ((s', ty), tm)]) =>
          (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
             possible, to work around LEO-II 1.2.8 parser limitation. *)
          string_for_formula format
              (AQuant (if s = tptp_ho_forall then AForall else AExists,
                       [(s', SOME ty)], AAtom tm))
+       | (_, true, [AAbs ((s', ty), tm)]) =>
+         (*There is code in ATP_Translate to ensure that Eps is always applied
+           to an abstraction*)
+         tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "] : " ^
+           string_for_term format tm ^ ""
+         |> enclose "(" ")"
+
        | _ =>
          let val ss = map (string_for_term format) ts in
            if is_format_thf format then
diff -r fbb777aec0d4 -r abcf7c0743e8 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 25 14:26:38 2011 -0700
@@ -216,11 +216,11 @@
      let val method = effective_e_weight_method ctxt in
        (* FUDGE *)
        if method = e_smartN then
-         [(0.333, (true, (500, FOF, "mangled_tags?", e_fun_weightN))),
-          (0.334, (true, (50, FOF, "mangled_guards?", e_fun_weightN))),
-          (0.333, (true, (1000, FOF, "mangled_tags?", e_sym_offset_weightN)))]
+         [(0.333, (true, (500, FOF, "mono_tags?", e_fun_weightN))),
+          (0.334, (true, (50, FOF, "mono_guards?", e_fun_weightN))),
+          (0.333, (true, (1000, FOF, "mono_tags?", e_sym_offset_weightN)))]
        else
-         [(1.0, (true, (500, FOF, "mangled_tags?", method)))]
+         [(1.0, (true, (500, FOF, "mono_tags?", method)))]
      end}
 
 val e = (eN, e_config)
@@ -293,9 +293,9 @@
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (150, FOF, "mangled_tags", sosN))),
+     [(0.333, (false, (150, FOF, "mono_tags", sosN))),
       (0.333, (false, (300, FOF, "poly_tags?", sosN))),
-      (0.334, (true, (50, FOF, "mangled_tags?", no_sosN)))]
+      (0.334, (true, (50, FOF, "mono_tags?", no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -324,7 +324,6 @@
      [(GaveUp, "UNPROVABLE"),
       (GaveUp, "CANNOT PROVE"),
       (GaveUp, "SZS status GaveUp"),
-      (ProofIncomplete, "predicate_definition_introduction,[]"),
       (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
       (Unprovable, "Termination reason: Satisfiable"),
@@ -336,8 +335,8 @@
      (* FUDGE *)
      (if is_old_vampire_version () then
         [(0.333, (false, (150, FOF, "poly_guards", sosN))),
-         (0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
-         (0.333, (false, (500, FOF, "mangled_tags?", sosN)))]
+         (0.334, (true, (50, FOF, "mono_guards?", no_sosN))),
+         (0.333, (false, (500, FOF, "mono_tags?", sosN)))]
       else
         [(0.333, (false, (150, TFF, "poly_guards", sosN))),
          (0.334, (true, (50, TFF, "simple", no_sosN))),
@@ -360,14 +359,15 @@
      [(GaveUp, "SZS status Satisfiable"),
       (GaveUp, "SZS status CounterSatisfiable"),
       (GaveUp, "SZS status GaveUp"),
+      (GaveUp, "SZS status Unknown"),
       (ProofMissing, "SZS status Unsatisfiable"),
       (ProofMissing, "SZS status Theorem")],
    conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(0.5, (false, (250, TFF, "simple", ""))),
-        (0.25, (false, (125, TFF, "simple", ""))),
+     K [(0.5, (false, (250, FOF, "mono_guards?", ""))),
+        (0.25, (false, (125, FOF, "mono_guards?", ""))),
         (0.125, (false, (62, TFF, "simple", ""))),
         (0.125, (false, (31, TFF, "simple", "")))]}
 
@@ -449,7 +449,7 @@
 
 val remote_e =
   remotify_atp e "EP" ["1.0", "1.1", "1.2"]
-               (K (750, FOF, "mangled_tags?") (* FUDGE *))
+               (K (750, FOF, "mono_tags?") (* FUDGE *))
 val remote_leo2 =
   remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
                (K (100, THF Without_Choice, "simple_higher") (* FUDGE *))
@@ -462,7 +462,7 @@
   remotify_atp z3_tptp "Z3" ["3.0"] (K (250, TFF, "simple") (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
-             Conjecture (K (500, FOF, "mangled_guards?") (* FUDGE *))
+             Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
@@ -476,7 +476,7 @@
              [(OutOfResources, "Too many function symbols"),
               (Crashed, "Unrecoverable Segmentation Fault")]
              Hypothesis Hypothesis
-             (K (50, CNF_UEQ, "mangled_tags?") (* FUDGE *))
+             (K (50, CNF_UEQ, "mono_tags?") (* FUDGE *))
 
 (* Setup *)
 
diff -r fbb777aec0d4 -r abcf7c0743e8 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 14:26:38 2011 -0700
@@ -20,7 +20,7 @@
     Chained
 
   datatype order = First_Order | Higher_Order
-  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+  datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
   datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
   datatype type_level =
     All_Types |
@@ -35,6 +35,8 @@
     Guards of polymorphism * type_level * type_uniformity |
     Tags of polymorphism * type_level * type_uniformity
 
+  val type_tag_idempotence : bool Config.T
+  val type_tag_arguments : bool Config.T
   val no_lambdasN : string
   val concealedN : string
   val liftingN : string
@@ -114,6 +116,11 @@
 
 type name = string * string
 
+val type_tag_idempotence =
+  Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K true)
+val type_tag_arguments =
+  Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K true)
+
 val no_lambdasN = "no_lambdas"
 val concealedN = "concealed"
 val liftingN = "lifting"
@@ -141,6 +148,7 @@
 val tfree_prefix = "t_"
 val const_prefix = "c_"
 val type_const_prefix = "tc_"
+val simple_type_prefix = "s_"
 val class_prefix = "cl_"
 
 val polymorphic_free_prefix = "poly_free"
@@ -165,11 +173,10 @@
 val untyped_helper_suffix = "_U"
 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
 
-val predicator_name = "p"
-val app_op_name = "a"
-val type_guard_name = "g"
-val type_tag_name = "t"
-val simple_type_prefix = "ty_"
+val predicator_name = "pp"
+val app_op_name = "aa"
+val type_guard_name = "gg"
+val type_tag_name = "tt"
 
 val prefixed_predicator_name = const_prefix ^ predicator_name
 val prefixed_app_op_name = const_prefix ^ app_op_name
@@ -308,8 +315,10 @@
 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
 
 (* "HOL.eq" is mapped to the ATP's equality. *)
-fun make_fixed_const @{const_name HOL.eq} = tptp_old_equal
-  | make_fixed_const c = const_prefix ^ lookup_const c
+fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
+  | make_fixed_const (SOME (THF With_Choice)) "Hilbert_Choice.Eps"(*FIXME*) =
+      tptp_choice
+  | make_fixed_const _ c = const_prefix ^ lookup_const c
 
 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
 
@@ -483,38 +492,38 @@
 
 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
    Also accumulates sort infomation. *)
-fun iterm_from_term thy bs (P $ Q) =
+fun iterm_from_term thy format bs (P $ Q) =
     let
-      val (P', P_atomics_Ts) = iterm_from_term thy bs P
-      val (Q', Q_atomics_Ts) = iterm_from_term thy bs Q
+      val (P', P_atomics_Ts) = iterm_from_term thy format bs P
+      val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q
     in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
-  | iterm_from_term thy _ (Const (c, T)) =
-    (IConst (`make_fixed_const c, T,
+  | iterm_from_term thy format _ (Const (c, T)) =
+    (IConst (`(make_fixed_const (SOME format)) c, T,
              if String.isPrefix old_skolem_const_prefix c then
                [] |> Term.add_tvarsT T |> map TVar
              else
                (c, T) |> Sign.const_typargs thy),
      atyps_of T)
-  | iterm_from_term _ _ (Free (s, T)) =
+  | iterm_from_term _ _ _ (Free (s, T)) =
     (IConst (`make_fixed_var s, T,
              if String.isPrefix polymorphic_free_prefix s then [T] else []),
      atyps_of T)
-  | iterm_from_term _ _ (Var (v as (s, _), T)) =
+  | iterm_from_term _ format _ (Var (v as (s, _), T)) =
     (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
        let
          val Ts = T |> strip_type |> swap |> op ::
          val s' = new_skolem_const_name s (length Ts)
-       in IConst (`make_fixed_const s', T, Ts) end
+       in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end
      else
        IVar ((make_schematic_var v, s), T), atyps_of T)
-  | iterm_from_term _ bs (Bound j) =
+  | iterm_from_term _ _ bs (Bound j) =
     nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atyps_of T))
-  | iterm_from_term thy bs (Abs (s, T, t)) =
+  | iterm_from_term thy format bs (Abs (s, T, t)) =
     let
       fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
       val s = vary s
       val name = `make_bound_var s
-      val (tm, atomic_Ts) = iterm_from_term thy ((s, (name, T)) :: bs) t
+      val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
     in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end
 
 datatype locality =
@@ -522,7 +531,7 @@
   Chained
 
 datatype order = First_Order | Higher_Order
-datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
 datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
 datatype type_level =
   All_Types |
@@ -544,10 +553,10 @@
   (case try (unprefix "poly_") s of
      SOME s => (SOME Polymorphic, s)
    | NONE =>
-     case try (unprefix "mono_") s of
-       SOME s => (SOME Monomorphic, s)
+     case try (unprefix "raw_mono_") s of
+       SOME s => (SOME Raw_Monomorphic, s)
      | NONE =>
-       case try (unprefix "mangled_") s of
+       case try (unprefix "mono_") s of
          SOME s => (SOME Mangled_Monomorphic, s)
        | NONE => (NONE, s))
   ||> (fn s =>
@@ -882,15 +891,20 @@
              | _ => IConst (name, T, [])
            else
              IConst (proxy_base |>> prefix const_prefix, T, T_args)
-          | NONE => IConst (name, T, T_args))
+          | NONE => if s = tptp_choice then
+                      (*this could be made neater by adding c_Eps as a proxy,
+                        but we'd need to be able to "see" Hilbert_Choice.Eps
+                        at this level in order to define fEps*)
+                      tweak_ho_quant tptp_choice T args
+                    else IConst (name, T, T_args))
       | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
       | intro _ _ tm = tm
   in intro true [] end
 
-fun iformula_from_prop thy type_enc eq_as_iff =
+fun iformula_from_prop thy format type_enc eq_as_iff =
   let
     fun do_term bs t atomic_types =
-      iterm_from_term thy bs (Envir.eta_contract t)
+      iterm_from_term thy format bs (Envir.eta_contract t)
       |>> (introduce_proxies type_enc #> AAtom)
       ||> union (op =) atomic_types
     fun do_quant bs q pos s T t' =
@@ -1041,10 +1055,10 @@
   end
 
 (* making fact and conjecture formulas *)
-fun make_formula thy type_enc eq_as_iff name loc kind t =
+fun make_formula thy format type_enc eq_as_iff name loc kind t =
   let
     val (iformula, atomic_types) =
-      iformula_from_prop thy type_enc eq_as_iff (SOME (kind <> Conjecture)) t []
+      iformula_from_prop thy format type_enc eq_as_iff (SOME (kind <> Conjecture)) t []
   in
     {name = name, locality = loc, kind = kind, iformula = iformula,
      atomic_types = atomic_types}
@@ -1052,8 +1066,8 @@
 
 fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
   let val thy = Proof_Context.theory_of ctxt in
-    case t |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
-                           loc Axiom of
+    case t |> make_formula thy format type_enc (eq_as_iff andalso format <> CNF)
+                           name loc Axiom of
       formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
       if s = tptp_true then NONE else SOME formula
     | formula => SOME formula
@@ -1065,7 +1079,7 @@
 fun make_conjecture thy format type_enc =
   map (fn ((name, loc), (kind, t)) =>
           t |> kind = Conjecture ? s_not_trueprop
-            |> make_formula thy type_enc (format <> CNF) name loc kind)
+            |> make_formula thy format type_enc (format <> CNF) name loc kind)
 
 (** Finite and infinite type inference **)
 
@@ -1097,17 +1111,15 @@
   | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
                              maybe_nonmono_Ts, ...}
                        (Noninf_Nonmono_Types soundness) T =
-    exists (type_instance ctxt T orf type_generalization ctxt T)
-           maybe_nonmono_Ts andalso
+    exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
     not (exists (type_instance ctxt T) surely_infinite_Ts orelse
          (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
           is_type_surely_infinite' ctxt soundness surely_infinite_Ts T))
   | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
                              maybe_nonmono_Ts, ...}
                        Fin_Nonmono_Types T =
-    exists (type_instance ctxt T orf type_generalization ctxt T)
-           maybe_nonmono_Ts andalso
-    (exists (type_instance ctxt T) surely_finite_Ts orelse
+    exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
+    (exists (type_generalization ctxt T) surely_finite_Ts orelse
      (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
       is_type_surely_finite ctxt T))
   | should_encode_type _ _ _ _ = false
@@ -1245,7 +1257,7 @@
 val default_sym_tab_entries : (string * sym_info) list =
   (prefixed_predicator_name,
    {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
-  (make_fixed_const @{const_name undefined},
+  (make_fixed_const NONE @{const_name undefined},
    {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
   ([tptp_false, tptp_true]
    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
@@ -1282,7 +1294,7 @@
   | NONE => false
 
 val predicator_combconst =
-  IConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
+  IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
 fun predicator tm = IApp (predicator_combconst, tm)
 
 fun introduce_predicators_in_iterm sym_tab tm =
@@ -1293,7 +1305,7 @@
 
 fun list_app head args = fold (curry (IApp o swap)) args head
 
-val app_op = `make_fixed_const app_op_name
+val app_op = `(make_fixed_const NONE) app_op_name
 
 fun explicit_app arg head =
   let
@@ -1348,7 +1360,8 @@
       | aux arity (IConst (name as (s, _), T, T_args)) =
         (case strip_prefix_and_unascii const_prefix s of
            NONE =>
-           (name, if level_of_type_enc type_enc = No_Types then [] else T_args)
+           (name, if level_of_type_enc type_enc = No_Types orelse s = tptp_choice
+                  then [] else T_args)
          | SOME s'' =>
            let
              val s'' = invert_const s''
@@ -1435,7 +1448,7 @@
   |> bound_tvars type_enc atomic_Ts
   |> close_formula_universally
 
-val type_tag = `make_fixed_const type_tag_name
+val type_tag = `(make_fixed_const NONE) type_tag_name
 
 fun type_tag_idempotence_fact type_enc =
   let
@@ -1449,7 +1462,7 @@
   end
 
 fun should_specialize_helper type_enc t =
-  polymorphism_of_type_enc type_enc = Mangled_Monomorphic andalso
+  polymorphism_of_type_enc type_enc <> Polymorphic andalso
   level_of_type_enc type_enc <> No_Types andalso
   not (null (Term.hidden_polymorphism t))
 
@@ -1582,7 +1595,7 @@
      (conjs, facts @ lambdas, class_rel_clauses, arity_clauses))
   end
 
-val type_guard = `make_fixed_const type_guard_name
+val type_guard = `(make_fixed_const NONE) type_guard_name
 
 fun type_guard_iterm ctxt format type_enc T tm =
   IApp (IConst (type_guard, T --> @{typ bool}, [T])
@@ -1792,7 +1805,7 @@
     fun add_undefined_const T =
       let
         val (s, s') =
-          `make_fixed_const @{const_name undefined}
+          `(make_fixed_const (SOME format)) @{const_name undefined}
           |> (case type_arg_policy type_enc @{const_name undefined} of
                 Mangled_Type_Args _ => mangled_const_name format type_enc [T]
               | _ => I)
@@ -1992,7 +2005,8 @@
       end
   in
     [] |> not pred_sym ? add_formula_for_res
-       |> fold add_formula_for_arg (ary - 1 downto 0)
+       |> Config.get ctxt type_tag_arguments
+          ? fold add_formula_for_arg (ary - 1 downto 0)
   end
 
 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
@@ -2054,11 +2068,12 @@
                syms []
   in mono_lines @ decl_lines end
 
-fun needs_type_tag_idempotence (Tags (poly, level, uniformity)) =
+fun needs_type_tag_idempotence ctxt (Tags (poly, level, uniformity)) =
+    Config.get ctxt type_tag_idempotence andalso
     poly <> Mangled_Monomorphic andalso
     ((level = All_Types andalso uniformity = Nonuniform) orelse
      is_type_level_monotonicity_based level)
-  | needs_type_tag_idempotence _ = false
+  | needs_type_tag_idempotence _ _ = false
 
 fun offset_of_heading_in_problem _ [] j = j
   | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
@@ -2128,7 +2143,7 @@
       0 upto length helpers - 1 ~~ helpers
       |> map (formula_line_for_fact ctxt format helper_prefix I false true mono
                                     type_enc)
-      |> (if needs_type_tag_idempotence type_enc then
+      |> (if needs_type_tag_idempotence ctxt type_enc then
             cons (type_tag_idempotence_fact type_enc)
           else
             I)
diff -r fbb777aec0d4 -r abcf7c0743e8 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 25 14:26:38 2011 -0700
@@ -17,6 +17,7 @@
   val string_from_time : Time.time -> string
   val type_instance : Proof.context -> typ -> typ -> bool
   val type_generalization : Proof.context -> typ -> typ -> bool
+  val type_intersect : Proof.context -> typ -> typ -> bool
   val type_aconv : Proof.context -> typ * typ -> bool
   val varify_type : Proof.context -> typ -> typ
   val instantiate_type : theory -> typ -> typ -> typ -> typ
@@ -117,6 +118,8 @@
 fun type_instance ctxt T T' =
   Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
 fun type_generalization ctxt T T' = type_instance ctxt T' T
+fun type_intersect ctxt T T' =
+  type_instance ctxt T T' orelse type_generalization ctxt T T'
 fun type_aconv ctxt (T, T') =
   type_instance ctxt T T' andalso type_instance ctxt T' T
 
diff -r fbb777aec0d4 -r abcf7c0743e8 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Aug 25 14:26:38 2011 -0700
@@ -9,14 +9,16 @@
 
 signature METIS_RECONSTRUCT =
 sig
+  type type_enc = ATP_Translate.type_enc
+
   exception METIS of string * string
 
   val hol_clause_from_metis :
-    Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
-    -> term
+    Proof.context -> type_enc -> int Symtab.table -> (string * term) list
+    -> Metis_Thm.thm -> term
   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
   val replay_one_inference :
-    Proof.context -> (string * term) list -> int Symtab.table
+    Proof.context -> type_enc -> (string * term) list -> int Symtab.table
     -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
     -> (Metis_Thm.thm * thm) list
   val discharge_skolem_premises :
@@ -33,38 +35,39 @@
 
 exception METIS of string * string
 
-fun atp_name_from_metis s =
-  case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
+fun atp_name_from_metis type_enc s =
+  case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
     SOME ((s, _), (_, swap)) => (s, swap)
   | _ => (s, false)
-fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
-    let val (s, swap) = atp_name_from_metis (Metis_Name.toString s) in
-      ATerm (s, tms |> map atp_term_from_metis |> swap ? rev)
+fun atp_term_from_metis type_enc (Metis_Term.Fn (s, tms)) =
+    let val (s, swap) = atp_name_from_metis type_enc (Metis_Name.toString s) in
+      ATerm (s, tms |> map (atp_term_from_metis type_enc) |> swap ? rev)
     end
-  | atp_term_from_metis (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
+  | atp_term_from_metis _ (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
 
-fun hol_term_from_metis ctxt sym_tab =
-  atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
+fun hol_term_from_metis ctxt type_enc sym_tab =
+  atp_term_from_metis type_enc #> term_from_atp ctxt false sym_tab NONE
 
-fun atp_literal_from_metis (pos, atom) =
-  atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot
-fun atp_clause_from_metis [] = AAtom (ATerm (tptp_false, []))
-  | atp_clause_from_metis lits =
-    lits |> map atp_literal_from_metis |> mk_aconns AOr
+fun atp_literal_from_metis type_enc (pos, atom) =
+  atom |> Metis_Term.Fn |> atp_term_from_metis type_enc
+       |> AAtom |> not pos ? mk_anot
+fun atp_clause_from_metis _ [] = AAtom (ATerm (tptp_false, []))
+  | atp_clause_from_metis type_enc lits =
+    lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
 
 fun reveal_old_skolems_and_infer_types ctxt old_skolems =
   map (reveal_old_skolem_terms old_skolems)
   #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
 
-fun hol_clause_from_metis ctxt sym_tab old_skolems =
+fun hol_clause_from_metis ctxt type_enc sym_tab old_skolems =
   Metis_Thm.clause
   #> Metis_LiteralSet.toList
-  #> atp_clause_from_metis
+  #> atp_clause_from_metis type_enc
   #> prop_from_atp ctxt false sym_tab
   #> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems)
 
-fun hol_terms_from_metis ctxt old_skolems sym_tab fol_tms =
-  let val ts = map (hol_term_from_metis ctxt sym_tab) fol_tms
+fun hol_terms_from_metis ctxt type_enc old_skolems sym_tab fol_tms =
+  let val ts = map (hol_term_from_metis ctxt type_enc sym_tab) fol_tms
       val _ = trace_msg ctxt (fn () => "  calling type inference:")
       val _ = app (fn t => trace_msg ctxt
                                      (fn () => Syntax.string_of_term ctxt t)) ts
@@ -111,10 +114,10 @@
       val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
   in  cterm_instantiate substs th  end;
 
-fun assume_inference ctxt old_skolems sym_tab atom =
+fun assume_inference ctxt type_enc old_skolems sym_tab atom =
   inst_excluded_middle
       (Proof_Context.theory_of ctxt)
-      (singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
+      (singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab)
                  (Metis_Term.Fn atom))
 
 (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
@@ -122,7 +125,7 @@
    sorts. Instead we try to arrange that new TVars are distinct and that types
    can be inferred from terms. *)
 
-fun inst_inference ctxt old_skolems sym_tab th_pairs fsubst th =
+fun inst_inference ctxt type_enc old_skolems sym_tab th_pairs fsubst th =
   let val thy = Proof_Context.theory_of ctxt
       val i_th = lookth th_pairs th
       val i_th_vars = Term.add_vars (prop_of i_th) []
@@ -130,7 +133,7 @@
       fun subst_translation (x,y) =
         let val v = find_var x
             (* We call "reveal_old_skolems_and_infer_types" below. *)
-            val t = hol_term_from_metis ctxt sym_tab y
+            val t = hol_term_from_metis ctxt type_enc sym_tab y
         in  SOME (cterm_of thy (Var v), t)  end
         handle Option.Option =>
                (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
@@ -255,7 +258,7 @@
 (* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
 val select_literal = negate_head oo make_last
 
-fun resolve_inference ctxt old_skolems sym_tab th_pairs atom th1 th2 =
+fun resolve_inference ctxt type_enc old_skolems sym_tab th_pairs atom th1 th2 =
   let
     val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
     val _ = trace_msg ctxt (fn () =>
@@ -271,7 +274,7 @@
       let
         val thy = Proof_Context.theory_of ctxt
         val i_atom =
-          singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
+          singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab)
                     (Metis_Term.Fn atom)
         val _ = trace_msg ctxt (fn () =>
                     "  atom: " ^ Syntax.string_of_term ctxt i_atom)
@@ -300,10 +303,11 @@
 val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
 val refl_idx = 1 + Thm.maxidx_of REFL_THM;
 
-fun refl_inference ctxt old_skolems sym_tab t =
+fun refl_inference ctxt type_enc old_skolems sym_tab t =
   let
     val thy = Proof_Context.theory_of ctxt
-    val i_t = singleton (hol_terms_from_metis ctxt old_skolems sym_tab) t
+    val i_t =
+      singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab) t
     val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
     val c_t = cterm_incr_types thy refl_idx i_t
   in cterm_instantiate [(refl_x, c_t)] REFL_THM end
@@ -313,11 +317,11 @@
 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
 
-fun equality_inference ctxt old_skolems sym_tab (pos, atom) fp fr =
+fun equality_inference ctxt type_enc old_skolems sym_tab (pos, atom) fp fr =
   let val thy = Proof_Context.theory_of ctxt
       val m_tm = Metis_Term.Fn atom
       val [i_atom, i_tm] =
-        hol_terms_from_metis ctxt old_skolems sym_tab [m_tm, fr]
+        hol_terms_from_metis ctxt type_enc old_skolems sym_tab [m_tm, fr]
       val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
       fun replace_item_list lx 0 (_::ls) = lx::ls
         | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
@@ -336,7 +340,8 @@
                                        #> the #> unmangled_const_name))
           in
             if s = metis_predicator orelse s = predicator_name orelse
-               s = metis_type_tag orelse s = type_tag_name then
+               s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag
+               orelse s = type_tag_name then
               path_finder tm ps (nth ts p)
             else if s = metis_app_op orelse s = app_op_name then
               let
@@ -377,21 +382,22 @@
 
 val factor = Seq.hd o distinct_subgoals_tac
 
-fun one_step ctxt old_skolems sym_tab th_pairs p =
+fun one_step ctxt type_enc old_skolems sym_tab th_pairs p =
   case p of
     (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
   | (_, Metis_Proof.Assume f_atom) =>
-    assume_inference ctxt old_skolems sym_tab f_atom
+    assume_inference ctxt type_enc old_skolems sym_tab f_atom
   | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
-    inst_inference ctxt old_skolems sym_tab th_pairs f_subst f_th1
+    inst_inference ctxt type_enc old_skolems sym_tab th_pairs f_subst f_th1
     |> factor
   | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
-    resolve_inference ctxt old_skolems sym_tab th_pairs f_atom f_th1 f_th2
+    resolve_inference ctxt type_enc old_skolems sym_tab th_pairs f_atom f_th1
+                      f_th2
     |> factor
   | (_, Metis_Proof.Refl f_tm) =>
-    refl_inference ctxt old_skolems sym_tab f_tm
+    refl_inference ctxt type_enc old_skolems sym_tab f_tm
   | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
-    equality_inference ctxt old_skolems sym_tab f_lit f_p f_r
+    equality_inference ctxt type_enc old_skolems sym_tab f_lit f_p f_r
 
 fun flexflex_first_order th =
   case Thm.tpairs_of th of
@@ -443,7 +449,8 @@
       end
   end
 
-fun replay_one_inference ctxt old_skolems sym_tab (fol_th, inf) th_pairs =
+fun replay_one_inference ctxt type_enc old_skolems sym_tab (fol_th, inf)
+                         th_pairs =
   if not (null th_pairs) andalso
      prop_of (snd (hd th_pairs)) aconv @{prop False} then
     (* Isabelle sometimes identifies literals (premises) that are distinct in
@@ -458,7 +465,7 @@
                   (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
       val _ = trace_msg ctxt
                   (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
-      val th = one_step ctxt old_skolems sym_tab th_pairs (fol_th, inf)
+      val th = one_step ctxt type_enc old_skolems sym_tab th_pairs (fol_th, inf)
                |> flexflex_first_order
                |> resynchronize ctxt fol_th
       val _ = trace_msg ctxt
diff -r fbb777aec0d4 -r abcf7c0743e8 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu Aug 25 14:26:38 2011 -0700
@@ -39,7 +39,7 @@
 val partial_typesN = "partial_types"
 val no_typesN = "no_types"
 
-val really_full_type_enc = "mangled_tags_uniform"
+val really_full_type_enc = "mono_tags_uniform"
 val full_type_enc = "poly_guards_uniform_query"
 val partial_type_enc = "poly_args"
 val no_type_enc = "erased"
@@ -74,9 +74,9 @@
    "t => t'", where "t" and "t'" are the same term modulo type tags.
    In Isabelle, type tags are stripped away, so we are left with "t = t" or
    "t => t". Type tag idempotence is also handled this way. *)
-fun reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth =
+fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth =
   let val thy = Proof_Context.theory_of ctxt in
-    case hol_clause_from_metis ctxt sym_tab old_skolems mth of
+    case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of
       Const (@{const_name HOL.eq}, _) $ _ $ t =>
       let
         val ct = cterm_of thy t
@@ -91,14 +91,7 @@
 
 fun clause_params type_enc =
   {ordering = Metis_KnuthBendixOrder.default,
-   orderLiterals =
-     (* Type axioms seem to benefit from the positive literal order, but for
-        compatibility we keep the unsigned order for Metis's default
-        "partial_types" mode. *)
-     if is_type_enc_fairly_sound type_enc then
-       Metis_Clause.PositiveLiteralOrder
-     else
-       Metis_Clause.UnsignedLiteralOrder,
+   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
    orderTerms = true}
 fun active_params type_enc =
   {clause = clause_params type_enc,
@@ -133,7 +126,7 @@
       val (sym_tab, axioms, old_skolems) =
         prepare_metis_problem ctxt type_enc cls ths
       fun get_isa_thm mth Isa_Reflexive_or_Trivial =
-          reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth
+          reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth
         | get_isa_thm _ (Isa_Raw ith) = ith
       val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
       val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
@@ -155,7 +148,7 @@
                 val proof = Metis_Proof.proof mth
                 val result =
                   axioms
-                  |> fold (replay_one_inference ctxt' old_skolems sym_tab) proof
+                  |> fold (replay_one_inference ctxt' type_enc old_skolems sym_tab) proof
                 val used = map_filter (used_axioms axioms) proof
                 val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
                 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
diff -r fbb777aec0d4 -r abcf7c0743e8 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Thu Aug 25 14:26:38 2011 -0700
@@ -18,13 +18,14 @@
   val metis_equal : string
   val metis_predicator : string
   val metis_app_op : string
-  val metis_type_tag : string
+  val metis_systematic_type_tag : string
+  val metis_ad_hoc_type_tag : string
   val metis_generated_var_prefix : string
   val trace : bool Config.T
   val verbose : bool Config.T
   val trace_msg : Proof.context -> (unit -> string) -> unit
   val verbose_warning : Proof.context -> string -> unit
-  val metis_name_table : ((string * int) * (string * bool)) list
+  val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
   val reveal_old_skolem_terms : (string * term) list -> term -> term
   val prepare_metis_problem :
     Proof.context -> type_enc -> thm list -> thm list
@@ -39,8 +40,10 @@
 
 val metis_equal = "="
 val metis_predicator = "{}"
-val metis_app_op = "."
-val metis_type_tag = ":"
+val metis_app_op = Metis_Name.toString Metis_Term.appName
+val metis_systematic_type_tag =
+  Metis_Name.toString Metis_Term.hasTypeFunctionName
+val metis_ad_hoc_type_tag = "**"
 val metis_generated_var_prefix = "_"
 
 val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
@@ -51,11 +54,13 @@
   if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
 
 val metis_name_table =
-  [((tptp_equal, 2), (metis_equal, false)),
-   ((tptp_old_equal, 2), (metis_equal, false)),
-   ((prefixed_predicator_name, 1), (metis_predicator, false)),
-   ((prefixed_app_op_name, 2), (metis_app_op, false)),
-   ((prefixed_type_tag_name, 2), (metis_type_tag, true))]
+  [((tptp_equal, 2), (K metis_equal, false)),
+   ((tptp_old_equal, 2), (K metis_equal, false)),
+   ((prefixed_predicator_name, 1), (K metis_predicator, false)),
+   ((prefixed_app_op_name, 2), (K metis_app_op, false)),
+   ((prefixed_type_tag_name, 2),
+    (fn Tags (_, All_Types, Uniform) => metis_systematic_type_tag
+      | _ => metis_ad_hoc_type_tag, true))]
 
 fun old_skolem_const_name i j num_T_args =
   old_skolem_const_prefix ^ Long_Name.separator ^
@@ -114,32 +119,34 @@
 val prepare_helper =
   Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
 
-fun metis_term_from_atp (ATerm (s, tms)) =
+fun metis_term_from_atp type_enc (ATerm (s, tms)) =
   if is_tptp_variable s then
     Metis_Term.Var (Metis_Name.fromString s)
   else
-    let
-      val (s, swap) = AList.lookup (op =) metis_name_table (s, length tms)
-                      |> the_default (s, false)
-    in
-      Metis_Term.Fn (Metis_Name.fromString s,
-                     tms |> map metis_term_from_atp |> swap ? rev)
-    end
-fun metis_atom_from_atp (AAtom tm) =
-    (case metis_term_from_atp tm of
+    (case AList.lookup (op =) metis_name_table (s, length tms) of
+       SOME (f, swap) => (f type_enc, swap)
+     | NONE => (s, false))
+    |> (fn (s, swap) =>
+           Metis_Term.Fn (Metis_Name.fromString s,
+                          tms |> map (metis_term_from_atp type_enc)
+                              |> swap ? rev))
+fun metis_atom_from_atp type_enc (AAtom tm) =
+    (case metis_term_from_atp type_enc tm of
        Metis_Term.Fn x => x
      | _ => raise Fail "non CNF -- expected function")
-  | metis_atom_from_atp _ = raise Fail "not CNF -- expected atom"
-fun metis_literal_from_atp (AConn (ANot, [phi])) =
-    (false, metis_atom_from_atp phi)
-  | metis_literal_from_atp phi = (true, metis_atom_from_atp phi)
-fun metis_literals_from_atp (AConn (AOr, phis)) =
-    maps metis_literals_from_atp phis
-  | metis_literals_from_atp phi = [metis_literal_from_atp phi]
-fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
+  | metis_atom_from_atp _ _ = raise Fail "not CNF -- expected atom"
+fun metis_literal_from_atp type_enc (AConn (ANot, [phi])) =
+    (false, metis_atom_from_atp type_enc phi)
+  | metis_literal_from_atp type_enc phi =
+    (true, metis_atom_from_atp type_enc phi)
+fun metis_literals_from_atp type_enc (AConn (AOr, phis)) =
+    maps (metis_literals_from_atp type_enc) phis
+  | metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi]
+fun metis_axiom_from_atp type_enc clauses (Formula (ident, _, phi, _, _)) =
     let
       fun some isa =
-        SOME (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
+        SOME (phi |> metis_literals_from_atp type_enc
+                  |> Metis_LiteralSet.fromList
                   |> Metis_Thm.axiom, isa)
     in
       if ident = type_tag_idempotence_helper_name orelse
@@ -164,7 +171,7 @@
         in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end
       | NONE => TrueI |> Isa_Raw |> some
     end
-  | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
+  | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
 
 (* Function to generate metis clauses, including comb and type clauses *)
 fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
@@ -205,8 +212,8 @@
     *)
     (* "rev" is for compatibility. *)
     val axioms =
-      atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
-                  |> rev
+      atp_problem
+      |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev
   in (sym_tab, axioms, old_skolems) end
 
 end;
diff -r fbb777aec0d4 -r abcf7c0743e8 src/HOL/Tools/SMT/z3_proof_parser.ML
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Thu Aug 25 14:26:38 2011 -0700
@@ -152,16 +152,14 @@
 
   fun prep (ct, vars) (maxidx, all_vars) =
     let
-      val maxidx' = maxidx_of ct + maxidx + 1
+      val maxidx' = maxidx + maxidx_of ct + 1
 
       fun part (v as (i, cv)) =
         (case AList.lookup (op =) all_vars i of
           SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu))
         | NONE =>
-            if not (exists (equal_var cv) all_vars) then apsnd (cons v)
-            else
-              let val cv' = Thm.incr_indexes_cterm maxidx' cv
-              in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end)
+            let val cv' = Thm.incr_indexes_cterm maxidx cv
+            in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end)
 
       val (inst, vars') =
         if null vars then ([], vars)
@@ -170,7 +168,7 @@
     in (Thm.instantiate_cterm ([], inst) ct, (maxidx', vars' @ all_vars)) end
 in
 fun mk_fun f ts =
-  let val (cts, (_, vars)) = fold_map prep ts (~1, [])
+  let val (cts, (_, vars)) = fold_map prep ts (0, [])
   in f cts |> Option.map (rpair vars) end
 end
 
diff -r fbb777aec0d4 -r abcf7c0743e8 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Thu Aug 25 14:26:38 2011 -0700
@@ -147,13 +147,15 @@
   val remove_weight = mk_meta_eq @{thm SMT.weight_def}
   val remove_fun_app = mk_meta_eq @{thm SMT.fun_app_def}
 
-  fun rewrite_conv ctxt eqs = Simplifier.full_rewrite
-    (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
+  fun rewrite_conv _ [] = Conv.all_conv
+    | rewrite_conv ctxt eqs = Simplifier.full_rewrite
+        (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
 
   val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
     remove_fun_app, Z3_Proof_Literals.rewrite_true]
 
-  fun rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
+  fun rewrite _ [] = I
+    | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
 
   fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm)
 
@@ -630,7 +632,8 @@
     in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end
 
   val sk_rules = @{lemma
-    "(EX x. P x) = P (SOME x. P x)"   "(~(ALL x. P x)) = (~P (SOME x. ~P x))"
+    "c = (SOME x. P x) ==> (EX x. P x) = P c"
+    "c = (SOME x. ~P x) ==> (~(ALL x. P x)) = (~P c)"
     by (metis someI_ex)+}
 in
 
@@ -638,9 +641,10 @@
   apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
 
 fun discharge_sk_tac i st = (
-  Tactic.rtac @{thm trans}
-  THEN' Tactic.resolve_tac sk_rules
-  THEN' (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac)) i st
+  Tactic.rtac @{thm trans} i
+  THEN Tactic.resolve_tac sk_rules i
+  THEN (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
+  THEN Tactic.rtac @{thm refl} i) st
 
 end
 
@@ -654,7 +658,7 @@
     Z3_Proof_Tools.by_tac (
       NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
       ORELSE' NAMED ctxt' "simp+arith" (
-        Simplifier.simp_tac simpset
+        Simplifier.asm_full_simp_tac simpset
         THEN_ALL_NEW Arith_Data.arith_tac ctxt')))]
 
 
@@ -717,13 +721,15 @@
         THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
     Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
       Z3_Proof_Tools.by_tac (
-        NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
+        (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+        THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
         THEN_ALL_NEW (
           NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
           ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
     Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
       Z3_Proof_Tools.by_tac (
-        NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
+        (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+        THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
         THEN_ALL_NEW (
           NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
           ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
@@ -731,7 +737,8 @@
     Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
       (fn ctxt' =>
         Z3_Proof_Tools.by_tac (
-          NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)
+          (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+          THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)
           THEN_ALL_NEW (
             NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
             ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac
diff -r fbb777aec0d4 -r abcf7c0743e8 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Aug 25 14:26:38 2011 -0700
@@ -148,7 +148,7 @@
                             | _ => value)
     | NONE => (name, value)
 
-(* Ensure that type systems such as "simple!" and "mangled_guards?" are handled
+(* Ensure that type systems such as "simple!" and "mono_guards?" are handled
    correctly. *)
 fun implode_param [s, "?"] = s ^ "?"
   | implode_param [s, "!"] = s ^ "!"