diff -r de6b601c8d3d -r 2eeb75cccb8d Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 15 22:36:59 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Jun 16 11:03:01 2011 +0100
@@ -295,11 +295,11 @@
   by (induct Ts T rule: lookup2.induct) simp_all
 
 nominal_primrec
-  subst  :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2"
+  subst2  :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2"
 where
-  "subst \<theta> (Var2 X) = lookup2 \<theta> X"
-| "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)"
-  unfolding eqvt_def subst_graph_def
+  "subst2 \<theta> (Var2 X) = lookup2 \<theta> X"
+| "subst2 \<theta> (Fun2 T1 T2) = Fun2 (subst2 \<theta> T1) (subst2 \<theta> T2)"
+  unfolding eqvt_def subst2_graph_def
   apply (rule, perm_simp, rule)
   apply(rule TrueI)
   apply(case_tac x)
@@ -310,11 +310,11 @@
   done
 
 termination
-  by (relation "measure (size o snd)") (simp_all add: ty2.size)
+  by lexicographic_order
 
 lemma subst_eqvt[eqvt]:
-  shows "(p \<bullet> subst \<theta> T) = subst (p \<bullet> \<theta>) (p \<bullet> T)"
-  by (induct \<theta> T rule: subst.induct) (simp_all add: lookup2_eqvt)
+  shows "(p \<bullet> subst2 \<theta> T) = subst2 (p \<bullet> \<theta>) (p \<bullet> T)"
+  by (induct \<theta> T rule: subst2.induct) (simp_all add: lookup2_eqvt)
 
 lemma supp_fun_app2_eqvt:
   assumes e: "eqvt f"
@@ -323,7 +323,7 @@
   by blast
  
 lemma supp_subst:
-  "supp (subst \<theta> t) \<subseteq> supp \<theta> \<union> supp t"
+  "supp (subst2 \<theta> t) \<subseteq> supp \<theta> \<union> supp t"
   apply (rule supp_fun_app2_eqvt)
   unfolding eqvt_def by (simp add: eqvts_raw)
  
@@ -332,10 +332,10 @@
   unfolding fresh_star_def by blast
 
 nominal_primrec
-  substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"
+  substs2 :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"
 where
-  "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)"
-  unfolding eqvt_def substs_graph_def
+  "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs2 \<theta> (All2 xs t) = All2 xs (subst2 \<theta> t)"
+  unfolding eqvt_def substs2_graph_def
   apply (rule, perm_simp, rule)
   apply auto[2]
   apply (rule_tac y="b" and c="a" in tys2.strong_exhaust)
@@ -354,7 +354,7 @@
   apply (rule_tac x="0::perm" in exI)
   apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
   apply (simp add: alphas fresh_star_zero)
-  apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")
+  apply (subgoal_tac "\<And>x. x \<in> supp (subst2 \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")
   apply blast
   apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> t)")
   apply (simp add: supp_Pair eqvts eqvts_raw)