diff -r f6b0d827240e -r bdc1e2f0a86a src/HOL/Metis_Examples/Clausification.thy
--- a/src/HOL/Metis_Examples/Clausification.thy	Tue Sep 01 17:25:36 2015 +0200
+++ b/src/HOL/Metis_Examples/Clausification.thy	Tue Sep 01 22:32:58 2015 +0200
@@ -140,7 +140,7 @@
 lemma ex_tl: "EX ys. tl ys = xs"
 using list.sel(3) by fast
 
-lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
+lemma "(\<exists>ys::nat list. tl ys = xs) \<and> (\<exists>bs::int list. tl bs = as)"
 by (metis ex_tl)
 
 end