src/HOL/Metis_Examples/Proxies.thy

 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)
-by (metisX id_apply)
+by (metisFT 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] ()
 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] ()
-by metisX
+by metisFT
 
 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)