--- a/src/HOL/Nominal/Examples/CK_Machine.thy Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy Mon Feb 21 17:43:23 2011 +0100
@@ -380,7 +380,7 @@
text {* Typing Contexts *}
-types tctx = "(name\<times>ty) list"
+type_synonym tctx = "(name\<times>ty) list"
text {* Sub-Typing Contexts *}
--- a/src/HOL/Nominal/Examples/Class1.thy Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/Class1.thy Mon Feb 21 17:43:23 2011 +0100
@@ -2912,9 +2912,8 @@
text {* typing contexts *}
-types
- ctxtn = "(name\<times>ty) list"
- ctxtc = "(coname\<times>ty) list"
+type_synonym ctxtn = "(name\<times>ty) list"
+type_synonym ctxtc = "(coname\<times>ty) list"
inductive
validc :: "ctxtc \<Rightarrow> bool"
--- a/src/HOL/Nominal/Examples/Crary.thy Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/Crary.thy Mon Feb 21 17:43:23 2011 +0100
@@ -25,8 +25,8 @@
| App "trm" "trm" ("App _ _" [110,110] 100)
| Const "nat"
-types Ctxt = "(name\<times>ty) list"
-types Subst = "(name\<times>trm) list"
+type_synonym Ctxt = "(name\<times>ty) list"
+type_synonym Subst = "(name\<times>trm) list"
lemma perm_ty[simp]:
--- a/src/HOL/Nominal/Examples/Fsub.thy Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy Mon Feb 21 17:43:23 2011 +0100
@@ -84,7 +84,7 @@
VarB vrs ty
| TVarB tyvrs ty
-types env = "binding list"
+type_synonym env = "binding list"
text {* Typing contexts are represented as lists that ``grow" on the left; we
thereby deviating from the convention in the POPLmark-paper. The lists contain
--- a/src/HOL/Nominal/Examples/LocalWeakening.thy Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/LocalWeakening.thy Mon Feb 21 17:43:23 2011 +0100
@@ -81,7 +81,7 @@
text {* valid contexts *}
-types cxt = "(name\<times>ty) list"
+type_synonym cxt = "(name\<times>ty) list"
inductive
valid :: "cxt \<Rightarrow> bool"
--- a/src/HOL/Nominal/Examples/Pattern.thy Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/Pattern.thy Mon Feb 21 17:43:23 2011 +0100
@@ -138,7 +138,7 @@
lemma pat_type_perm_eq: "pat_type ((pi :: name prm) \<bullet> p) = pat_type p"
by (induct p) (simp_all add: perm_type)
-types ctx = "(name \<times> ty) list"
+type_synonym ctx = "(name \<times> ty) list"
inductive
ptyping :: "pat \<Rightarrow> ty \<Rightarrow> ctx \<Rightarrow> bool" ("\<turnstile> _ : _ \<Rightarrow> _" [60, 60, 60] 60)
--- a/src/HOL/Nominal/Examples/Type_Preservation.thy Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Examples/Type_Preservation.thy Mon Feb 21 17:43:23 2011 +0100
@@ -58,7 +58,7 @@
text {* Typing Contexts *}
-types ctx = "(name\<times>ty) list"
+type_synonym ctx = "(name\<times>ty) list"
abbreviation
"sub_ctx" :: "ctx \<Rightarrow> ctx \<Rightarrow> bool" ("_ \<subseteq> _")
--- 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)
--- a/src/HOL/Nominal/Nominal.thy Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nominal/Nominal.thy Mon Feb 21 17:43:23 2011 +0100
@@ -15,7 +15,7 @@
section {* Permutations *}
(*======================*)
-types
+type_synonym
'x prm = "('x \<times> 'x) list"
(* polymorphic constants for permutation and swapping *)