# HG changeset patch
# User blanchet
# Date 1309528418 -7200
# Node ID a867ebb122090121741bfebe35160eea59fd5bdb
# Parent  c3e28c86949999b6bdecd3e4e8cc92c7fd861031
renamed "type_sys" to "type_enc", which is more accurate

diff -r c3e28c869499 -r a867ebb12209 src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy	Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy	Fri Jul 01 15:53:38 2011 +0200
@@ -50,215 +50,215 @@
 by linarith
 
 lemma "B \<subseteq> C"
-sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some]
+sledgehammer [type_enc = poly_args, max_relevant = 200, expect = some]
 by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
 
 
 text {* Proxies for logical constants *}
 
 lemma "id (op =) x x"
-sledgehammer [type_sys = erased, expect = none] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = none] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis (full_types) id_apply)
 
 lemma "id True"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "\<not> id False"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "x = id True \<or> x = id False"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id x = id True \<or> id x = id False"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
-sledgehammer [type_sys = erased, expect = none] ()
-sledgehammer [type_sys = poly_args, expect = none] ()
-sledgehammer [type_sys = poly_tags?, expect = some] ()
-sledgehammer [type_sys = poly_tags, expect = some] ()
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] ()
-sledgehammer [type_sys = mangled_tags?, expect = some] ()
-sledgehammer [type_sys = mangled_tags, expect = some] ()
-sledgehammer [type_sys = mangled_preds?, expect = some] ()
-sledgehammer [type_sys = mangled_preds, expect = some] ()
+sledgehammer [type_enc = erased, expect = none] ()
+sledgehammer [type_enc = poly_args, expect = none] ()
+sledgehammer [type_enc = poly_tags?, expect = some] ()
+sledgehammer [type_enc = poly_tags, expect = some] ()
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] ()
+sledgehammer [type_enc = mangled_tags?, expect = some] ()
+sledgehammer [type_enc = mangled_tags, expect = some] ()
+sledgehammer [type_enc = mangled_preds?, expect = some] ()
+sledgehammer [type_enc = mangled_preds, expect = some] ()
 by (metis (full_types))
 
 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (a \<and> b) \<Longrightarrow> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (a \<and> b) \<Longrightarrow> id b"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id a \<Longrightarrow> id (a \<or> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id b \<Longrightarrow> id (a \<or> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 end
diff -r c3e28c869499 -r a867ebb12209 src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Fri Jul 01 15:53:38 2011 +0200
@@ -24,7 +24,7 @@
 ML {*
 (* The commented-out type systems are too incomplete for our exhaustive
    tests. *)
-val type_syss =
+val type_encs =
   ["erased",
    "poly_preds",
    "poly_preds_heavy",
@@ -72,18 +72,18 @@
 fun metis_exhaust_tac ctxt ths =
   let
     fun tac [] st = all_tac st
-      | tac (type_sys :: type_syss) st =
-        st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *)
-           |> ((if null type_syss then all_tac else rtac @{thm fork} 1)
-               THEN Metis_Tactics.metis_tac [type_sys] ctxt ths 1
+      | tac (type_enc :: type_encs) st =
+        st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *)
+           |> ((if null type_encs then all_tac else rtac @{thm fork} 1)
+               THEN Metis_Tactics.metis_tac [type_enc] ctxt ths 1
                THEN COND (has_fewer_prems 2) all_tac no_tac
-               THEN tac type_syss)
+               THEN tac type_encs)
   in tac end
 *}
 
 method_setup metis_exhaust = {*
   Attrib.thms >>
-    (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_syss))
+    (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_encs))
 *} "exhaustively run the new Metis with all type encodings"
 
 
diff -r c3e28c869499 -r a867ebb12209 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jul 01 15:53:38 2011 +0200
@@ -8,7 +8,7 @@
 val proverK = "prover"
 val prover_timeoutK = "prover_timeout"
 val keepK = "keep"
-val type_sysK = "type_sys"
+val type_encK = "type_enc"
 val slicingK = "slicing"
 val e_weight_methodK = "e_weight_method"
 val spass_force_sosK = "spass_force_sos"
@@ -353,7 +353,7 @@
   SH_FAIL of int * int |
   SH_ERROR
 
-fun run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos
+fun run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
       vampire_force_sos hard_timeout timeout dir st =
   let
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
@@ -377,7 +377,7 @@
     val params as {relevance_thresholds, max_relevant, slicing, ...} =
       Sledgehammer_Isar.default_params ctxt
           [("verbose", "true"),
-           ("type_sys", type_sys),
+           ("type_enc", type_enc),
            ("max_relevant", max_relevant),
            ("slicing", slicing),
            ("timeout", string_of_int timeout)]
@@ -452,7 +452,7 @@
     val _ = change_data id inc_sh_calls
     val _ = if trivial then () else change_data id inc_sh_nontriv_calls
     val (prover_name, prover) = get_prover (Proof.context_of st) args
-    val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
+    val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
     val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
     val slicing = AList.lookup (op =) args slicingK |> the_default "true"
     val e_weight_method = AList.lookup (op =) args e_weight_methodK
@@ -466,7 +466,7 @@
        minimizer has a chance to do its magic *)
     val hard_timeout = SOME (2 * timeout)
     val (msg, result) =
-      run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos
+      run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
         vampire_force_sos hard_timeout timeout dir st
   in
     case result of
@@ -503,7 +503,7 @@
     val ctxt = Proof.context_of st
     val n0 = length (these (!named_thms))
     val (prover_name, _) = get_prover ctxt args
-    val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
+    val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
     val timeout =
       AList.lookup (op =) args minimize_timeoutK
       |> Option.map (fst o read_int o raw_explode)  (* FIXME Symbol.explode (?) *)
@@ -511,7 +511,7 @@
     val params = Sledgehammer_Isar.default_params ctxt
       [("provers", prover_name),
        ("verbose", "true"),
-       ("type_sys", type_sys),
+       ("type_enc", type_enc),
        ("timeout", string_of_int timeout)]
     val minimize =
       Sledgehammer_Minimize.minimize_facts prover_name params
@@ -546,9 +546,9 @@
        else if !reconstructor = "smt" then
          SMT_Solver.smt_tac
        else if full orelse !reconstructor = "metis (full_types)" then
-         Metis_Tactics.metis_tac [Metis_Tactics.full_type_sys]
+         Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc]
        else if !reconstructor = "metis (no_types)" then
-         Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys]
+         Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
        else
          Metis_Tactics.metis_tac []) ctxt thms
     fun apply_reconstructor thms =
diff -r c3e28c869499 -r a867ebb12209 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 01 15:53:38 2011 +0200
@@ -386,8 +386,8 @@
    prem_kind = prem_kind,
    formats = formats,
    best_slices = fn ctxt =>
-     let val (max_relevant, type_sys) = best_slice ctxt in
-       [(1.0, (false, (max_relevant, type_sys, "")))]
+     let val (max_relevant, type_enc) = best_slice ctxt in
+       [(1.0, (false, (max_relevant, type_enc, "")))]
      end}
 
 fun remotify_config system_name system_versions best_slice
diff -r c3e28c869499 -r a867ebb12209 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Jul 01 15:53:38 2011 +0200
@@ -26,7 +26,7 @@
     No_Types
   datatype type_heaviness = Heavyweight | Lightweight
 
-  datatype type_sys =
+  datatype type_enc =
     Simple_Types of order * type_level |
     Preds of polymorphism * type_level * type_heaviness |
     Tags of polymorphism * type_level * type_heaviness
@@ -75,12 +75,12 @@
   val atp_irrelevant_consts : string list
   val atp_schematic_consts_of : term -> typ list Symtab.table
   val is_locality_global : locality -> bool
-  val type_sys_from_string : string -> type_sys
-  val polymorphism_of_type_sys : type_sys -> polymorphism
-  val level_of_type_sys : type_sys -> type_level
-  val is_type_sys_virtually_sound : type_sys -> bool
-  val is_type_sys_fairly_sound : type_sys -> bool
-  val choose_format : format list -> type_sys -> format * type_sys
+  val type_enc_from_string : string -> type_enc
+  val polymorphism_of_type_enc : type_enc -> polymorphism
+  val level_of_type_enc : type_enc -> type_level
+  val is_type_enc_virtually_sound : type_enc -> bool
+  val is_type_enc_fairly_sound : type_enc -> bool
+  val choose_format : format list -> type_enc -> format * type_enc
   val mk_aconns :
     connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
   val unmangled_const : string -> string * string fo_term list
@@ -88,7 +88,7 @@
   val helper_table : ((string * bool) * thm list) list
   val factsN : string
   val prepare_atp_problem :
-    Proof.context -> format -> formula_kind -> formula_kind -> type_sys -> bool
+    Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
     -> bool -> bool -> bool -> term list -> term
     -> ((string * locality) * term) list
     -> string problem * string Symtab.table * int * int
@@ -509,7 +509,7 @@
   No_Types
 datatype type_heaviness = Heavyweight | Lightweight
 
-datatype type_sys =
+datatype type_enc =
   Simple_Types of order * type_level |
   Preds of polymorphism * type_level * type_heaviness |
   Tags of polymorphism * type_level * type_heaviness
@@ -517,7 +517,7 @@
 fun try_unsuffixes ss s =
   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
 
-fun type_sys_from_string s =
+fun type_enc_from_string s =
   (case try (unprefix "poly_") s of
      SOME s => (SOME Polymorphic, s)
    | NONE =>
@@ -557,29 +557,29 @@
          | _ => raise Same.SAME)
   handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
 
-fun is_type_sys_higher_order (Simple_Types (Higher_Order, _)) = true
-  | is_type_sys_higher_order _ = false
+fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true
+  | is_type_enc_higher_order _ = false
 
-fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
-  | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
-  | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
+fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
+  | polymorphism_of_type_enc (Preds (poly, _, _)) = poly
+  | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
 
-fun level_of_type_sys (Simple_Types (_, level)) = level
-  | level_of_type_sys (Preds (_, level, _)) = level
-  | level_of_type_sys (Tags (_, level, _)) = level
+fun level_of_type_enc (Simple_Types (_, level)) = level
+  | level_of_type_enc (Preds (_, level, _)) = level
+  | level_of_type_enc (Tags (_, level, _)) = level
 
-fun heaviness_of_type_sys (Simple_Types _) = Heavyweight
-  | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
-  | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
+fun heaviness_of_type_enc (Simple_Types _) = Heavyweight
+  | heaviness_of_type_enc (Preds (_, _, heaviness)) = heaviness
+  | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
 
 fun is_type_level_virtually_sound level =
   level = All_Types orelse level = Noninf_Nonmono_Types
-val is_type_sys_virtually_sound =
-  is_type_level_virtually_sound o level_of_type_sys
+val is_type_enc_virtually_sound =
+  is_type_level_virtually_sound o level_of_type_enc
 
 fun is_type_level_fairly_sound level =
   is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
-val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
+val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
 
 fun choose_format formats (Simple_Types (order, level)) =
     if member (op =) formats THF then
@@ -588,15 +588,15 @@
       (TFF, Simple_Types (First_Order, level))
     else
       choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
-  | choose_format formats type_sys =
+  | choose_format formats type_enc =
     (case hd formats of
        CNF_UEQ =>
-       (CNF_UEQ, case type_sys of
+       (CNF_UEQ, case type_enc of
                    Preds stuff =>
-                   (if is_type_sys_fairly_sound type_sys then Tags else Preds)
+                   (if is_type_enc_fairly_sound type_enc then Tags else Preds)
                        stuff
-                 | _ => type_sys)
-     | format => (format, type_sys))
+                 | _ => type_enc)
+     | format => (format, type_enc))
 
 type translated_formula =
   {name : string,
@@ -628,30 +628,30 @@
 
 fun should_drop_arg_type_args (Simple_Types _) =
     false (* since TFF doesn't support overloading *)
-  | should_drop_arg_type_args type_sys =
-    level_of_type_sys type_sys = All_Types andalso
-    heaviness_of_type_sys type_sys = Heavyweight
+  | should_drop_arg_type_args type_enc =
+    level_of_type_enc type_enc = All_Types andalso
+    heaviness_of_type_enc type_enc = Heavyweight
 
 fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args
-  | general_type_arg_policy type_sys =
-    if level_of_type_sys type_sys = No_Types then
+  | general_type_arg_policy type_enc =
+    if level_of_type_enc type_enc = No_Types then
       No_Type_Args
-    else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
-      Mangled_Type_Args (should_drop_arg_type_args type_sys)
+    else if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
+      Mangled_Type_Args (should_drop_arg_type_args type_enc)
     else
-      Explicit_Type_Args (should_drop_arg_type_args type_sys)
+      Explicit_Type_Args (should_drop_arg_type_args type_enc)
 
-fun type_arg_policy type_sys s =
+fun type_arg_policy type_enc s =
   if s = @{const_name HOL.eq} orelse
-     (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
+     (s = app_op_name andalso level_of_type_enc type_enc = Const_Arg_Types) then
     No_Type_Args
   else if s = type_tag_name then
-    (if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
+    (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
        Mangled_Type_Args
      else
        Explicit_Type_Args) false
   else
-    general_type_arg_policy type_sys
+    general_type_arg_policy type_enc
 
 (*Make literals for sorted type variables*)
 fun generic_add_sorts_on_type (_, []) = I
@@ -669,8 +669,8 @@
 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
   | add_sorts_on_tvar _ = I
 
-fun type_literals_for_types type_sys add_sorts_on_typ Ts =
-  [] |> level_of_type_sys type_sys <> No_Types ? fold add_sorts_on_typ Ts
+fun type_literals_for_types type_enc add_sorts_on_typ Ts =
+  [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
 
 fun mk_aconns c phis =
   let val (phis', phi') = split_last phis in
@@ -705,10 +705,10 @@
 val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
 val homo_infinite_type = Type (homo_infinite_type_name, [])
 
-fun fo_term_from_typ format type_sys =
+fun fo_term_from_typ format type_enc =
   let
     fun term (Type (s, Ts)) =
-      ATerm (case (is_type_sys_higher_order type_sys, s) of
+      ATerm (case (is_type_enc_higher_order type_enc, s) of
                (true, @{type_name bool}) => `I tptp_bool_type
              | (true, @{type_name fun}) => `I tptp_fun_type
              | _ => if s = homo_infinite_type_name andalso
@@ -722,8 +722,8 @@
       ATerm ((make_schematic_type_var x, s), [])
   in term end
 
-fun fo_term_for_type_arg format type_sys T =
-  if T = dummyT then NONE else SOME (fo_term_from_typ format type_sys T)
+fun fo_term_for_type_arg format type_enc T =
+  if T = dummyT then NONE else SOME (fo_term_from_typ format type_enc T)
 
 (* This shouldn't clash with anything else. *)
 val mangled_type_sep = "\000"
@@ -742,7 +742,7 @@
   else
     simple_type_prefix ^ ascii_of s
 
-fun ho_type_from_fo_term type_sys pred_sym ary =
+fun ho_type_from_fo_term type_enc pred_sym ary =
   let
     fun to_atype ty =
       AType ((make_simple_type (generic_mangled_type_name fst ty),
@@ -752,15 +752,15 @@
       | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
     fun to_ho (ty as ATerm ((s, _), tys)) =
       if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
-  in if is_type_sys_higher_order type_sys then to_ho else to_fo ary end
+  in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
 
-fun mangled_type format type_sys pred_sym ary =
-  ho_type_from_fo_term type_sys pred_sym ary
-  o fo_term_from_typ format type_sys
+fun mangled_type format type_enc pred_sym ary =
+  ho_type_from_fo_term type_enc pred_sym ary
+  o fo_term_from_typ format type_enc
 
-fun mangled_const_name format type_sys T_args (s, s') =
+fun mangled_const_name format type_enc T_args (s, s') =
   let
-    val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_sys)
+    val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_enc)
     fun type_suffix f g =
       fold_rev (curry (op ^) o g o prefix mangled_type_sep
                 o generic_mangled_type_name f) ty_args ""
@@ -789,14 +789,14 @@
     (hd ss, map unmangled_type (tl ss))
   end
 
-fun introduce_proxies type_sys =
+fun introduce_proxies type_enc =
   let
     fun intro top_level (CombApp (tm1, tm2)) =
         CombApp (intro top_level tm1, intro false tm2)
       | intro top_level (CombConst (name as (s, _), T, T_args)) =
         (case proxify_const s of
            SOME proxy_base =>
-           if top_level orelse is_type_sys_higher_order type_sys then
+           if top_level orelse is_type_enc_higher_order type_enc then
              case (top_level, s) of
                (_, "c_False") => (`I tptp_false, [])
              | (_, "c_True") => (`I tptp_true, [])
@@ -815,11 +815,11 @@
       | intro _ tm = tm
   in intro true end
 
-fun combformula_from_prop thy type_sys eq_as_iff =
+fun combformula_from_prop thy type_enc eq_as_iff =
   let
     fun do_term bs t atomic_types =
       combterm_from_term thy bs (Envir.eta_contract t)
-      |>> (introduce_proxies type_sys #> AAtom)
+      |>> (introduce_proxies type_enc #> AAtom)
       ||> union (op =) atomic_types
     fun do_quant bs q s T t' =
       let val s = singleton (Name.variant_list (map fst bs)) s in
@@ -940,27 +940,27 @@
   end
 
 (* making fact and conjecture formulas *)
-fun make_formula thy type_sys eq_as_iff name loc kind t =
+fun make_formula thy type_enc eq_as_iff name loc kind t =
   let
     val (combformula, atomic_types) =
-      combformula_from_prop thy type_sys eq_as_iff t []
+      combformula_from_prop thy type_enc eq_as_iff t []
   in
     {name = name, locality = loc, kind = kind, combformula = combformula,
      atomic_types = atomic_types}
   end
 
-fun make_fact ctxt format type_sys eq_as_iff preproc presimp_consts
+fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts
               ((name, loc), t) =
   let val thy = Proof_Context.theory_of ctxt in
     case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
-           |> make_formula thy type_sys (eq_as_iff andalso format <> CNF) name
+           |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
                            loc Axiom of
       formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
       if s = tptp_true then NONE else SOME formula
     | formula => SOME formula
   end
 
-fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts =
+fun make_conjecture ctxt format prem_kind type_enc preproc presimp_consts ts =
   let
     val thy = Proof_Context.theory_of ctxt
     val last = length ts - 1
@@ -977,7 +977,7 @@
               in
                 t |> preproc ?
                      (preprocess_prop ctxt presimp_consts kind #> freeze_term)
-                  |> make_formula thy type_sys (format <> CNF) (string_of_int j)
+                  |> make_formula thy type_enc (format <> CNF) (string_of_int j)
                                   Local kind
                   |> maybe_negate
               end)
@@ -1231,7 +1231,7 @@
     end
     handle TYPE _ => T_args
 
-fun enforce_type_arg_policy_in_combterm ctxt format type_sys =
+fun enforce_type_arg_policy_in_combterm ctxt format type_enc =
   let
     val thy = Proof_Context.theory_of ctxt
     fun aux arity (CombApp (tm1, tm2)) =
@@ -1245,11 +1245,11 @@
              fun filtered_T_args false = T_args
                | filtered_T_args true = filter_type_args thy s'' arity T_args
            in
-             case type_arg_policy type_sys s'' of
+             case type_arg_policy type_enc s'' of
                Explicit_Type_Args drop_args =>
                (name, filtered_T_args drop_args)
              | Mangled_Type_Args drop_args =>
-               (mangled_const_name format type_sys (filtered_T_args drop_args)
+               (mangled_const_name format type_enc (filtered_T_args drop_args)
                                    name, [])
              | No_Type_Args => (name, [])
            end)
@@ -1257,14 +1257,14 @@
       | aux _ tm = tm
   in aux 0 end
 
-fun repair_combterm ctxt format type_sys sym_tab =
-  not (is_type_sys_higher_order type_sys)
+fun repair_combterm ctxt format type_enc sym_tab =
+  not (is_type_enc_higher_order type_enc)
   ? (introduce_explicit_apps_in_combterm sym_tab
      #> introduce_predicators_in_combterm sym_tab)
-  #> enforce_type_arg_policy_in_combterm ctxt format type_sys
-fun repair_fact ctxt format type_sys sym_tab =
+  #> enforce_type_arg_policy_in_combterm ctxt format type_enc
+fun repair_fact ctxt format type_enc sym_tab =
   update_combformula (formula_map
-      (repair_combterm ctxt format type_sys sym_tab))
+      (repair_combterm ctxt format type_enc sym_tab))
 
 (** Helper facts **)
 
@@ -1313,12 +1313,12 @@
              |> close_formula_universally, simp_info, NONE)
   end
 
-fun should_specialize_helper type_sys t =
-  case general_type_arg_policy type_sys of
+fun should_specialize_helper type_enc t =
+  case general_type_arg_policy type_enc of
     Mangled_Type_Args _ => not (null (Term.hidden_polymorphism t))
   | _ => false
 
-fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
+fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
   case strip_prefix_and_unascii const_prefix s of
     SOME mangled_s =>
     let
@@ -1331,14 +1331,14 @@
            else untyped_helper_suffix),
           Helper),
          let val t = th |> prop_of in
-           t |> should_specialize_helper type_sys t
+           t |> should_specialize_helper type_enc t
                 ? (case types of
                      [T] => specialize_type thy (invert_const unmangled_s, T)
                    | _ => I)
          end)
       val make_facts =
-        map_filter (make_fact ctxt format type_sys false false [])
-      val fairly_sound = is_type_sys_fairly_sound type_sys
+        map_filter (make_fact ctxt format type_enc false false [])
+      val fairly_sound = is_type_enc_fairly_sound type_enc
     in
       helper_table
       |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
@@ -1351,8 +1351,8 @@
                     |> make_facts)
     end
   | NONE => []
-fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
-  Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
+fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
+  Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
                   []
 
 (***************************************************************)
@@ -1393,13 +1393,13 @@
 fun type_constrs_of_terms thy ts =
   Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
 
-fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
+fun translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
                        facts =
   let
     val thy = Proof_Context.theory_of ctxt
     val fact_ts = facts |> map snd
     val presimp_consts = Meson.presimplified_consts ctxt
-    val make_fact = make_fact ctxt format type_sys true preproc presimp_consts
+    val make_fact = make_fact ctxt format type_enc true preproc presimp_consts
     val (facts, fact_names) =
       facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
             |> map_filter (try (apfst the))
@@ -1416,9 +1416,9 @@
     val tycons = type_constrs_of_terms thy all_ts
     val conjs =
       hyp_ts @ [concl_t]
-      |> make_conjecture ctxt format prem_kind type_sys preproc presimp_consts
+      |> make_conjecture ctxt format prem_kind type_enc preproc presimp_consts
     val (supers', arity_clauses) =
-      if level_of_type_sys type_sys = No_Types then ([], [])
+      if level_of_type_enc type_enc = No_Types then ([], [])
       else make_arity_clauses thy tycons supers
     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   in
@@ -1434,9 +1434,9 @@
 
 val type_pred = `make_fixed_const type_pred_name
 
-fun type_pred_combterm ctxt format type_sys T tm =
+fun type_pred_combterm ctxt format type_enc T tm =
   CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
-           |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm)
+           |> enforce_type_arg_policy_in_combterm ctxt format type_enc, tm)
 
 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
   | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
@@ -1445,15 +1445,15 @@
     formula_fold pos (is_var_positively_naked_in_term name) phi false
   | should_predicate_on_var_in_formula _ _ _ _ = true
 
-fun mk_const_aterm format type_sys x T_args args =
-  ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args)
+fun mk_const_aterm format type_enc x T_args args =
+  ATerm (x, map_filter (fo_term_for_type_arg format type_enc) T_args @ args)
 
-fun tag_with_type ctxt format nonmono_Ts type_sys pos T tm =
+fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
   CombConst (type_tag, T --> T, [T])
-  |> enforce_type_arg_policy_in_combterm ctxt format type_sys
-  |> term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
+  |> enforce_type_arg_policy_in_combterm ctxt format type_enc
+  |> term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
   |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
-and term_from_combterm ctxt format nonmono_Ts type_sys =
+and term_from_combterm ctxt format nonmono_Ts type_enc =
   let
     fun aux site u =
       let
@@ -1469,32 +1469,32 @@
             (pos, if is_tptp_equal s then Eq_Arg pos else Elsewhere)
           | Eq_Arg pos => (pos, Elsewhere)
           | Elsewhere => (NONE, Elsewhere)
-        val t = mk_const_aterm format type_sys x T_args
+        val t = mk_const_aterm format type_enc x T_args
                     (map (aux arg_site) args)
         val T = combtyp_of u
       in
-        t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
-                tag_with_type ctxt format nonmono_Ts type_sys pos T
+        t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
+                tag_with_type ctxt format nonmono_Ts type_enc pos T
               else
                 I)
       end
   in aux end
-and formula_from_combformula ctxt format nonmono_Ts type_sys
+and formula_from_combformula ctxt format nonmono_Ts type_enc
                              should_predicate_on_var =
   let
     fun do_term pos =
-      term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
+      term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
     val do_bound_type =
-      case type_sys of
+      case type_enc of
         Simple_Types (_, level) =>
         homogenized_type ctxt nonmono_Ts level 0
-        #> mangled_type format type_sys false 0 #> SOME
+        #> mangled_type format type_enc false 0 #> SOME
       | _ => K NONE
     fun do_out_of_bound_type pos phi universal (name, T) =
-      if should_predicate_on_type ctxt nonmono_Ts type_sys
+      if should_predicate_on_type ctxt nonmono_Ts type_enc
              (fn () => should_predicate_on_var pos phi universal name) T then
         CombVar (name, T)
-        |> type_pred_combterm ctxt format type_sys T
+        |> type_pred_combterm ctxt format type_enc T
         |> do_term pos |> AAtom |> SOME
       else
         NONE
@@ -1517,23 +1517,23 @@
       | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
   in do_formula end
 
-fun bound_tvars type_sys Ts =
+fun bound_tvars type_enc Ts =
   mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
-                (type_literals_for_types type_sys add_sorts_on_tvar Ts))
+                (type_literals_for_types type_enc add_sorts_on_tvar Ts))
 
 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    of monomorphization). The TPTP explicitly forbids name clashes, and some of
    the remote provers might care. *)
 fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
-        type_sys (j, {name, locality, kind, combformula, atomic_types}) =
+        type_enc (j, {name, locality, kind, combformula, atomic_types}) =
   (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name,
    kind,
    combformula
    |> close_combformula_universally
-   |> formula_from_combformula ctxt format nonmono_Ts type_sys
+   |> formula_from_combformula ctxt format nonmono_Ts type_enc
                                should_predicate_on_var_in_formula
                                (if pos then SOME true else NONE)
-   |> bound_tvars type_sys atomic_types
+   |> bound_tvars type_enc atomic_types
    |> close_formula_universally,
    NONE,
    case locality of
@@ -1566,45 +1566,45 @@
                          (fo_literal_from_arity_literal concl_lits))
            |> close_formula_universally, intro_info, NONE)
 
-fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
+fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc
         ({name, kind, combformula, atomic_types, ...} : translated_formula) =
   Formula (conjecture_prefix ^ name, kind,
-           formula_from_combformula ctxt format nonmono_Ts type_sys
+           formula_from_combformula ctxt format nonmono_Ts type_enc
                should_predicate_on_var_in_formula (SOME false)
                (close_combformula_universally combformula)
-           |> bound_tvars type_sys atomic_types
+           |> bound_tvars type_enc atomic_types
            |> close_formula_universally, NONE, NONE)
 
-fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
-  atomic_types |> type_literals_for_types type_sys add_sorts_on_tfree
+fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) =
+  atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree
                |> map fo_literal_from_type_literal
 
 fun formula_line_for_free_type j lit =
   Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
            formula_from_fo_literal lit, NONE, NONE)
-fun formula_lines_for_free_types type_sys facts =
+fun formula_lines_for_free_types type_enc facts =
   let
-    val litss = map (free_type_literals type_sys) facts
+    val litss = map (free_type_literals type_enc) facts
     val lits = fold (union (op =)) litss []
   in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
 
 (** Symbol declarations **)
 
-fun should_declare_sym type_sys pred_sym s =
+fun should_declare_sym type_enc pred_sym s =
   is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
-  (case type_sys of
+  (case type_enc of
      Simple_Types _ => true
    | Tags (_, _, Lightweight) => true
    | _ => not pred_sym)
 
-fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
+fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) =
   let
     fun add_combterm in_conj tm =
       let val (head, args) = strip_combterm_comb tm in
         (case head of
            CombConst ((s, s'), T, T_args) =>
            let val pred_sym = is_pred_sym repaired_sym_tab s in
-             if should_declare_sym type_sys pred_sym s then
+             if should_declare_sym type_enc pred_sym s then
                Symtab.map_default (s, [])
                    (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
                                          in_conj))
@@ -1618,7 +1618,7 @@
       fact_lift (formula_fold NONE (K (add_combterm in_conj)))
   in
     Symtab.empty
-    |> is_type_sys_fairly_sound type_sys
+    |> is_type_enc_fairly_sound type_enc
        ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
   end
 
@@ -1641,8 +1641,8 @@
   formula_fold (SOME (kind <> Conjecture))
                (add_combterm_nonmonotonic_types ctxt level sound locality)
                combformula
-fun nonmonotonic_types_for_facts ctxt type_sys sound facts =
-  let val level = level_of_type_sys type_sys in
+fun nonmonotonic_types_for_facts ctxt type_enc sound facts =
+  let val level = level_of_type_enc type_enc in
     if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
       [] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts
          (* We must add "bool" in case the helper "True_or_False" is added
@@ -1653,21 +1653,21 @@
       []
   end
 
-fun decl_line_for_sym ctxt format nonmono_Ts type_sys s
+fun decl_line_for_sym ctxt format nonmono_Ts type_enc s
                       (s', T_args, T, pred_sym, ary, _) =
   let
     val (T_arg_Ts, level) =
-      case type_sys of
+      case type_enc of
         Simple_Types (_, level) => ([], level)
       | _ => (replicate (length T_args) homo_infinite_type, No_Types)
   in
     Decl (sym_decl_prefix ^ s, (s, s'),
           (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
-          |> mangled_type format type_sys pred_sym (length T_arg_Ts + ary))
+          |> mangled_type format type_enc pred_sym (length T_arg_Ts + ary))
   end
 
 fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
-        poly_nonmono_Ts type_sys n s j (s', T_args, T, _, ary, in_conj) =
+        poly_nonmono_Ts type_enc n s j (s', T_args, T, _, ary, in_conj) =
   let
     val (kind, maybe_negate) =
       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
@@ -1681,7 +1681,7 @@
     val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args
     fun should_keep_arg_type T =
       sym_needs_arg_types orelse
-      not (should_predicate_on_type ctxt nonmono_Ts type_sys (K false) T)
+      not (should_predicate_on_type ctxt nonmono_Ts type_enc (K false) T)
     val bound_Ts =
       arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
   in
@@ -1689,18 +1689,18 @@
              (if n > 1 then "_" ^ string_of_int j else ""), kind,
              CombConst ((s, s'), T, T_args)
              |> fold (curry (CombApp o swap)) bounds
-             |> type_pred_combterm ctxt format type_sys res_T
+             |> type_pred_combterm ctxt format type_enc res_T
              |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
-             |> formula_from_combformula ctxt format poly_nonmono_Ts type_sys
+             |> formula_from_combformula ctxt format poly_nonmono_Ts type_enc
                                          (K (K (K (K true)))) (SOME true)
-             |> n > 1 ? bound_tvars type_sys (atyps_of T)
+             |> n > 1 ? bound_tvars type_enc (atyps_of T)
              |> close_formula_universally
              |> maybe_negate,
              intro_info, NONE)
   end
 
 fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
-        poly_nonmono_Ts type_sys n s
+        poly_nonmono_Ts type_enc n s
         (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   let
     val ident_base =
@@ -1713,22 +1713,22 @@
     val bound_names =
       1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
     val bounds = bound_names |> map (fn name => ATerm (name, []))
-    val cst = mk_const_aterm format type_sys (s, s') T_args
+    val cst = mk_const_aterm format type_enc (s, s') T_args
     val atomic_Ts = atyps_of T
     fun eq tms =
       (if pred_sym then AConn (AIff, map AAtom tms)
        else AAtom (ATerm (`I tptp_equal, tms)))
-      |> bound_tvars type_sys atomic_Ts
+      |> bound_tvars type_enc atomic_Ts
       |> close_formula_universally
       |> maybe_negate
     (* See also "should_tag_with_type". *)
     fun should_encode T =
       should_encode_type ctxt poly_nonmono_Ts All_Types T orelse
-      (case type_sys of
+      (case type_enc of
          Tags (Polymorphic, level, Lightweight) =>
          level <> All_Types andalso Monomorph.typ_has_tvars T
        | _ => false)
-    val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_sys NONE
+    val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_enc NONE
     val add_formula_for_res =
       if should_encode res_T then
         cons (Formula (ident_base ^ "_res", kind,
@@ -1757,10 +1757,10 @@
 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
 
 fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
-                                poly_nonmono_Ts type_sys (s, decls) =
-  case type_sys of
+                                poly_nonmono_Ts type_enc (s, decls) =
+  case type_enc of
     Simple_Types _ =>
-    decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
+    decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
   | Preds _ =>
     let
       val decls =
@@ -1776,13 +1776,13 @@
         | _ => decls
       val n = length decls
       val decls =
-        decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_sys
+        decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_enc
                                                   (K true)
                          o result_type_of_decl)
     in
       (0 upto length decls - 1, decls)
       |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
-                   nonmono_Ts poly_nonmono_Ts type_sys n s)
+                   nonmono_Ts poly_nonmono_Ts type_enc n s)
     end
   | Tags (_, _, heaviness) =>
     (case heaviness of
@@ -1791,17 +1791,17 @@
        let val n = length decls in
          (0 upto n - 1 ~~ decls)
          |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
-                      conj_sym_kind poly_nonmono_Ts type_sys n s)
+                      conj_sym_kind poly_nonmono_Ts type_enc n s)
        end)
 
 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
-                                     poly_nonmono_Ts type_sys sym_decl_tab =
+                                     poly_nonmono_Ts type_enc sym_decl_tab =
   sym_decl_tab
   |> Symtab.dest
   |> sort_wrt fst
   |> rpair []
   |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
-                             nonmono_Ts poly_nonmono_Ts type_sys)
+                             nonmono_Ts poly_nonmono_Ts type_enc)
 
 fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
     poly <> Mangled_Monomorphic andalso
@@ -1825,39 +1825,39 @@
 
 val explicit_apply = NONE (* for experimental purposes *)
 
-fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys sound
+fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
         exporter readable_names preproc hyp_ts concl_t facts =
   let
-    val (format, type_sys) = choose_format [format] type_sys
+    val (format, type_enc) = choose_format [format] type_enc
     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
-      translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
+      translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
                          facts
     val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
     val nonmono_Ts =
-      conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys sound
-    val repair = repair_fact ctxt format type_sys sym_tab
+      conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc sound
+    val repair = repair_fact ctxt format type_enc sym_tab
     val (conjs, facts) = (conjs, facts) |> pairself (map repair)
     val repaired_sym_tab =
       conjs @ facts |> sym_table_for_facts ctxt (SOME false)
     val helpers =
-      repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
+      repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
                        |> map repair
     val poly_nonmono_Ts =
       if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
-         polymorphism_of_type_sys type_sys <> Polymorphic then
+         polymorphism_of_type_enc type_enc <> Polymorphic then
         nonmono_Ts
       else
         [TVar (("'a", 0), HOLogic.typeS)]
     val sym_decl_lines =
       (conjs, helpers @ facts)
-      |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
+      |> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab
       |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
-                                               poly_nonmono_Ts type_sys
+                                               poly_nonmono_Ts type_enc
     val helper_lines =
       0 upto length helpers - 1 ~~ helpers
       |> map (formula_line_for_fact ctxt format helper_prefix I false true
-                                    poly_nonmono_Ts type_sys)
-      |> (if needs_type_tag_idempotence type_sys then
+                                    poly_nonmono_Ts type_enc)
+      |> (if needs_type_tag_idempotence type_enc then
             cons (type_tag_idempotence_fact ())
           else
             I)
@@ -1868,15 +1868,15 @@
        (factsN,
         map (formula_line_for_fact ctxt format fact_prefix ascii_of
                                    (not exporter) (not exporter) nonmono_Ts
-                                   type_sys)
+                                   type_enc)
             (0 upto length facts - 1 ~~ facts)),
        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
        (aritiesN, map formula_line_for_arity_clause arity_clauses),
        (helpersN, helper_lines),
        (conjsN,
-        map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
+        map (formula_line_for_conjecture ctxt format nonmono_Ts type_enc)
             conjs),
-       (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
+       (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
     val problem =
       problem
       |> (case format of
diff -r c3e28c869499 -r a867ebb12209 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Fri Jul 01 15:53:38 2011 +0200
@@ -13,10 +13,10 @@
   val full_typesN : string
   val partial_typesN : string
   val no_typesN : string
-  val really_full_type_sys : string
-  val full_type_sys : string
-  val partial_type_sys : string
-  val no_type_sys : string
+  val really_full_type_enc : string
+  val full_type_enc : string
+  val partial_type_enc : string
+  val no_type_enc : string
   val full_type_syss : string list
   val partial_type_syss : string list
   val trace : bool Config.T
@@ -39,22 +39,22 @@
 val partial_typesN = "partial_types"
 val no_typesN = "no_types"
 
-val really_full_type_sys = "poly_tags_heavy"
-val full_type_sys = "poly_preds_heavy_query"
-val partial_type_sys = "poly_args"
-val no_type_sys = "erased"
+val really_full_type_enc = "poly_tags_heavy"
+val full_type_enc = "poly_preds_heavy_query"
+val partial_type_enc = "poly_args"
+val no_type_enc = "erased"
 
-val full_type_syss = [full_type_sys, really_full_type_sys]
-val partial_type_syss = partial_type_sys :: full_type_syss
+val full_type_syss = [full_type_enc, really_full_type_enc]
+val partial_type_syss = partial_type_enc :: full_type_syss
 
-val type_sys_aliases =
+val type_enc_aliases =
   [(full_typesN, full_type_syss),
    (partial_typesN, partial_type_syss),
-   (no_typesN, [no_type_sys])]
+   (no_typesN, [no_type_enc])]
 
-fun method_call_for_type_sys type_syss =
+fun method_call_for_type_enc type_syss =
   metisN ^ " (" ^
-  (case AList.find (op =) type_sys_aliases type_syss of
+  (case AList.find (op =) type_enc_aliases type_syss of
      [alias] => alias
    | _ => hd type_syss) ^ ")"
 
@@ -102,7 +102,7 @@
 val resolution_params = {active = active_params, waiting = waiting_params}
 
 (* Main function to start Metis proof and reconstruction *)
-fun FOL_SOLVE (type_sys :: fallback_type_syss) ctxt cls ths0 =
+fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
   let val thy = Proof_Context.theory_of ctxt
       val new_skolemizer =
         Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
@@ -118,7 +118,7 @@
       val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
       val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
       val (sym_tab, axioms, old_skolems) =
-        prepare_metis_problem ctxt type_sys cls ths
+        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
         | get_isa_thm _ (Isa_Raw ith) = ith
@@ -126,7 +126,7 @@
       val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
       val thms = axioms |> map fst
       val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
-      val _ = trace_msg ctxt (fn () => "type_sys = " ^ type_sys)
+      val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
       val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
   in
       case filter (fn t => prop_of t aconv @{prop False}) cls of
@@ -186,7 +186,7 @@
          | _ =>
            (verbose_warning ctxt
                 ("Falling back on " ^
-                 quote (method_call_for_type_sys fallback_type_syss) ^ "...");
+                 quote (method_call_for_type_enc fallback_type_syss) ^ "...");
             FOL_SOLVE fallback_type_syss ctxt cls ths0)
 
 val neg_clausify =
@@ -249,7 +249,7 @@
 
 fun setup_method (binding, type_syss) =
   ((Args.parens (Scan.repeat Parse.short_ident)
-    >> maps (fn s => case AList.lookup (op =) type_sys_aliases s of
+    >> maps (fn s => case AList.lookup (op =) type_enc_aliases s of
                        SOME tss => tss
                      | NONE => [s]))
     |> Scan.option |> Scan.lift)
diff -r c3e28c869499 -r a867ebb12209 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Fri Jul 01 15:53:38 2011 +0200
@@ -165,11 +165,11 @@
   | 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_sys conj_clauses fact_clauses =
+fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
   let
-    val type_sys = type_sys_from_string type_sys
+    val type_enc = type_enc_from_string type_enc
     val (conj_clauses, fact_clauses) =
-      if polymorphism_of_type_sys type_sys = Polymorphic then
+      if polymorphism_of_type_enc type_enc = Polymorphic then
         (conj_clauses, fact_clauses)
       else
         conj_clauses @ fact_clauses
@@ -196,7 +196,7 @@
       tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
     *)
     val (atp_problem, _, _, _, _, _, sym_tab) =
-      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys true false false
+      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false false
                           false [] @{prop False} props
     (*
     val _ = tracing ("ATP PROBLEM: " ^
diff -r c3e28c869499 -r a867ebb12209 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 01 15:53:38 2011 +0200
@@ -84,7 +84,7 @@
    ("verbose", "false"),
    ("overlord", "false"),
    ("blocking", "false"),
-   ("type_sys", "smart"),
+   ("type_enc", "smart"),
    ("sound", "false"),
    ("relevance_thresholds", "0.45 0.85"),
    ("max_relevant", "smart"),
@@ -107,7 +107,7 @@
    ("no_slicing", "slicing")]
 
 val params_for_minimize =
-  ["debug", "verbose", "overlord", "type_sys", "sound", "max_mono_iters",
+  ["debug", "verbose", "overlord", "type_enc", "sound", "max_mono_iters",
    "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
    "preplay_timeout"]
 
@@ -124,15 +124,15 @@
     ss as _ :: _ => forall (is_prover_supported ctxt) ss
   | _ => false
 
-(* "provers =" and "type_sys =" can be left out. The latter is a secret
+(* "provers =" and "type_enc =" can be left out. The latter is a secret
    feature. *)
 fun check_and_repair_raw_param ctxt (name, value) =
   if is_known_raw_param name then
     (name, value)
   else if is_prover_list ctxt name andalso null value then
     ("provers", [name])
-  else if can type_sys_from_string name andalso null value then
-    ("type_sys", [name])
+  else if can type_enc_from_string name andalso null value then
+    ("type_enc", [name])
   else
     error ("Unknown parameter: " ^ quote name ^ ".")
 
@@ -264,12 +264,12 @@
       lookup_bool "blocking"
     val provers = lookup_string "provers" |> space_explode " "
                   |> mode = Auto_Try ? single o hd
-    val type_sys =
+    val type_enc =
       if mode = Auto_Try then
         NONE
-      else case lookup_string "type_sys" of
+      else case lookup_string "type_enc" of
         "smart" => NONE
-      | s => SOME (type_sys_from_string s)
+      | s => SOME (type_enc_from_string s)
     val sound = mode = Auto_Try orelse lookup_bool "sound"
     val relevance_thresholds = lookup_real_pair "relevance_thresholds"
     val max_relevant = lookup_option lookup_int "max_relevant"
@@ -288,7 +288,7 @@
     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
      provers = provers, relevance_thresholds = relevance_thresholds,
      max_relevant = max_relevant, max_mono_iters = max_mono_iters,
-     max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
+     max_new_mono_instances = max_new_mono_instances, type_enc = type_enc,
      sound = sound, isar_proof = isar_proof,
      isar_shrink_factor = isar_shrink_factor, slicing = slicing,
      timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
diff -r c3e28c869499 -r a867ebb12209 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 01 15:53:38 2011 +0200
@@ -47,7 +47,7 @@
 fun print silent f = if silent then () else Output.urgent_message (f ())
 
 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
-                 max_new_mono_instances, type_sys, isar_proof,
+                 max_new_mono_instances, type_enc, isar_proof,
                  isar_shrink_factor, preplay_timeout, ...} : params)
                silent (prover : prover) timeout i n state facts =
   let
@@ -59,7 +59,7 @@
     val {goal, ...} = Proof.goal state
     val params =
       {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
-       provers = provers, type_sys = type_sys, sound = true,
+       provers = provers, type_enc = type_enc, sound = true,
        relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
        max_mono_iters = max_mono_iters,
        max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
diff -r c3e28c869499 -r a867ebb12209 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jul 01 15:53:38 2011 +0200
@@ -10,7 +10,7 @@
 sig
   type failure = ATP_Proof.failure
   type locality = ATP_Translate.locality
-  type type_sys = ATP_Translate.type_sys
+  type type_enc = ATP_Translate.type_enc
   type reconstructor = ATP_Reconstruct.reconstructor
   type play = ATP_Reconstruct.play
   type minimize_command = ATP_Reconstruct.minimize_command
@@ -24,7 +24,7 @@
      overlord: bool,
      blocking: bool,
      provers: string list,
-     type_sys: type_sys option,
+     type_enc: type_enc option,
      sound: bool,
      relevance_thresholds: real * real,
      max_relevant: int option,
@@ -289,7 +289,7 @@
    overlord: bool,
    blocking: bool,
    provers: string list,
-   type_sys: type_sys option,
+   type_enc: type_enc option,
    sound: bool,
    relevance_thresholds: real * real,
    max_relevant: int option,
@@ -407,11 +407,11 @@
   in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
 
 fun tac_for_reconstructor Metis =
-    Metis_Tactics.metis_tac [Metis_Tactics.partial_type_sys]
+    Metis_Tactics.metis_tac [Metis_Tactics.partial_type_enc]
   | tac_for_reconstructor Metis_Full_Types =
     Metis_Tactics.metis_tac Metis_Tactics.full_type_syss
   | tac_for_reconstructor Metis_No_Types =
-    Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys]
+    Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
   | tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
 
 fun timed_reconstructor reconstructor debug timeout ths =
@@ -504,10 +504,10 @@
    them each time. *)
 val atp_important_message_keep_quotient = 10
 
-fun choose_format_and_type_sys best_type_sys formats type_sys_opt =
-  (case type_sys_opt of
+fun choose_format_and_type_enc best_type_enc formats type_enc_opt =
+  (case type_enc_opt of
      SOME ts => ts
-   | NONE => type_sys_from_string best_type_sys)
+   | NONE => type_enc_from_string best_type_enc)
   |> choose_format formats
 
 val metis_minimize_max_time = seconds 2.0
@@ -530,7 +530,7 @@
 fun run_atp mode name
         ({exec, required_execs, arguments, proof_delims, known_failures,
           conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
-        ({debug, verbose, overlord, type_sys, sound, max_relevant,
+        ({debug, verbose, overlord, type_enc, sound, max_relevant,
           max_mono_iters, max_new_mono_instances, isar_proof,
           isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
         minimize_command
@@ -598,21 +598,21 @@
                 |> maps (fn (name, rths) => map (pair name o snd) rths)
               end
             fun run_slice (slice, (time_frac, (complete,
-                                    (best_max_relevant, best_type_sys, extra))))
+                                    (best_max_relevant, best_type_enc, extra))))
                           time_left =
               let
                 val num_facts =
                   length facts |> is_none max_relevant
                                   ? Integer.min best_max_relevant
-                val (format, type_sys) =
-                  choose_format_and_type_sys best_type_sys formats type_sys
-                val fairly_sound = is_type_sys_fairly_sound type_sys
+                val (format, type_enc) =
+                  choose_format_and_type_enc best_type_enc formats type_enc
+                val fairly_sound = is_type_enc_fairly_sound type_enc
                 val facts =
                   facts |> map untranslated_fact
                         |> not fairly_sound
                            ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
                         |> take num_facts
-                        |> polymorphism_of_type_sys type_sys <> Polymorphic
+                        |> polymorphism_of_type_enc type_enc <> Polymorphic
                            ? monomorphize_facts
                         |> map (apsnd prop_of)
                 val real_ms = Real.fromInt o Time.toMilliseconds
@@ -635,7 +635,7 @@
                 val (atp_problem, pool, conjecture_offset, facts_offset,
                      fact_names, typed_helpers, sym_tab) =
                   prepare_atp_problem ctxt format conj_sym_kind prem_kind
-                      type_sys sound false (Config.get ctxt atp_readable_names)
+                      type_enc sound false (Config.get ctxt atp_readable_names)
                       true hyp_ts concl_t facts
                 fun weights () = atp_problem_weights atp_problem
                 val full_proof = debug orelse isar_proof
@@ -675,7 +675,7 @@
                     used_facts_in_unsound_atp_proof ctxt
                         conjecture_shape facts_offset fact_names atp_proof
                     |> Option.map (fn facts =>
-                           UnsoundProof (is_type_sys_virtually_sound type_sys,
+                           UnsoundProof (is_type_enc_virtually_sound type_enc,
                                          facts |> sort string_ord))
                   | _ => outcome
               in
diff -r c3e28c869499 -r a867ebb12209 src/HOL/ex/atp_export.ML
--- a/src/HOL/ex/atp_export.ML	Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/ex/atp_export.ML	Fri Jul 01 15:53:38 2011 +0200
@@ -149,17 +149,17 @@
     if heading = factsN then (heading, order_facts ord lines) :: problem
     else (heading, lines) :: order_problem_facts ord problem
 
-fun generate_tptp_inference_file_for_theory ctxt thy type_sys file_name =
+fun generate_tptp_inference_file_for_theory ctxt thy type_enc file_name =
   let
     val format = FOF
-    val type_sys = type_sys |> type_sys_from_string
+    val type_enc = type_enc |> type_enc_from_string
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val facts = facts_of thy
     val (atp_problem, _, _, _, _, _, _) =
       facts
       |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
-      |> prepare_atp_problem ctxt format Axiom Axiom type_sys true true false
+      |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true false
                              true [] @{prop False}
     val atp_problem =
       atp_problem