diff -r 0c6093d596d6 -r c3aa3c87ef21 src/HOL/Nominal/Examples/W.thy
--- a/src/HOL/Nominal/Examples/W.thy	Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/W.thy	Mon Feb 21 17:43:23 2011 +0100
@@ -53,7 +53,7 @@
 where
  "Let x be t1 in t2 \<equiv> trm.Let x t2 t1"
 
-types 
+type_synonym 
   Ctxt  = "(var\<times>tyS) list" 
 
 text {* free type variables *}
@@ -173,7 +173,7 @@
   
 text {* Substitution *}
 
-types Subst = "(tvar\<times>ty) list"
+type_synonym Subst = "(tvar\<times>ty) list"
 
 consts
   psubst :: "Subst \<Rightarrow> 'a \<Rightarrow> 'a"       ("_<_>" [100,60] 120)