# HG changeset patch
# User blanchet
# Date 1314275107 -7200
# Node ID a77901b3774ec75174d5298700b37ff15ceb7a90
# Parent  c2602c5d4b0a756f26f24cdab5f7114aee068d9e
rationalized option names -- mono becomes raw_mono and mangled becomes mono

diff -r c2602c5d4b0a -r a77901b3774e doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Aug 25 14:25:07 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Aug 25 14:25:07 2011 +0200
@@ -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 c2602c5d4b0a -r a77901b3774e src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy	Thu Aug 25 14:25:07 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy	Thu Aug 25 14:25:07 2011 +0200
@@ -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 c2602c5d4b0a -r a77901b3774e src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Thu Aug 25 14:25:07 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Thu Aug 25 14:25:07 2011 +0200
@@ -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 c2602c5d4b0a -r a77901b3774e src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 25 14:25:07 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 25 14:25:07 2011 +0200
@@ -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)}
 
@@ -335,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))),
@@ -448,7 +448,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 *))
@@ -461,7 +461,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
@@ -475,7 +475,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 c2602c5d4b0a -r a77901b3774e src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 14:25:07 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 14:25:07 2011 +0200
@@ -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 |
@@ -522,7 +522,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 +544,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 =>
diff -r c2602c5d4b0a -r a77901b3774e src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu Aug 25 14:25:07 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu Aug 25 14:25:07 2011 +0200
@@ -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"
diff -r c2602c5d4b0a -r a77901b3774e src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Aug 25 14:25:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Aug 25 14:25:07 2011 +0200
@@ -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 ^ "!"