1.1 --- a/src/HOL/Metis_Examples/Proxies.thy	Tue Jun 07 07:57:24 2011 +0200
     1.2 +++ b/src/HOL/Metis_Examples/Proxies.thy	Tue Jun 07 08:52:35 2011 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
     1.5  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
     1.6  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
     1.7 -by (metisFT id_apply)
     1.8 +by (metis (full_types) id_apply)
     1.9  
    1.10  lemma "id True"
    1.11  sledgehammer [type_sys = erased, expect = some] (id_apply)
    1.12 @@ -127,7 +127,7 @@
    1.13  sledgehammer [type_sys = mangled_tags, expect = some] ()
    1.14  sledgehammer [type_sys = mangled_preds?, expect = some] ()
    1.15  sledgehammer [type_sys = mangled_preds, expect = some] ()
    1.16 -by metisFT
    1.17 +by (metis (full_types))
    1.18  
    1.19  lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
    1.20  sledgehammer [type_sys = erased, expect = some] (id_apply)