diff -r a609eea06119 -r d0ad264f8c4f Nominal/Ex/LF.thy
--- a/Nominal/Ex/LF.thy	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/Ex/LF.thy	Thu Nov 03 13:19:23 2011 +0000
@@ -55,9 +55,9 @@
     TC_ass "ident" "kind"
   | C_ass "ident" "ty"
 
-types Sig = "sig_ass list"
-types Ctx = "(name \<times> ty) list"
-types Subst = "(name \<times> trm) list"
+type_synonym Sig = "sig_ass list"
+type_synonym Ctx = "(name \<times> ty) list"
+type_synonym Subst = "(name \<times> trm) list"
 
 inductive
     sig_valid  :: "Sig \<Rightarrow> bool" ("\<turnstile> _ sig" [60] 60)