--- a/Nominal/Ex/SFT/Consts.thy	Fri Jul 22 11:52:12 2011 +0100
+++ b/Nominal/Ex/SFT/Consts.thy	Sun Jul 24 07:54:54 2011 +0200
@@ -94,13 +94,7 @@
     by (rule, perm_simp, rule)
 qed
 
-termination
-  by (relation "measure (\<lambda>(t). size t)")
-     (simp_all add: lam.size)
-
-lemma numeral_eqvt[eqvt]: "p \<bullet> \<lbrace>x\<rbrace> = \<lbrace>p \<bullet> x\<rbrace>"
-  by (induct x rule: lam.induct)
-     (simp_all add: Var_App_Abs_eqvt)
+termination (eqvt) by lexicographic_order
 
 lemma supp_numeral[simp]:
   "supp \<lbrace>x\<rbrace> = supp x"
@@ -145,27 +139,7 @@
   apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev)
   done
 
-termination
-  by (relation "measure (\<lambda>t. size t)")
-     (simp_all add: lam.size)
-
-lemma ltgt_eqvt[eqvt]:
-  "p \<bullet> \<guillemotleft>t\<guillemotright> = \<guillemotleft>p \<bullet> t\<guillemotright>"
-proof -
-  obtain x :: var where "atom x \<sharp> (t, p \<bullet> t)" using obtain_fresh by auto
-  then have *: "atom x \<sharp> t" "atom x \<sharp> (p \<bullet> t)" using fresh_Pair by simp_all
-  then show ?thesis using *[unfolded fresh_def]
-    apply (simp add: Abs1_eq_iff lam.fresh app_lst_eqvt Ltgt.simps)
-    apply (case_tac "p \<bullet> x = x")
-    apply (simp_all add: eqvts)
-    apply rule
-    apply (subst swap_fresh_fresh)
-    apply (simp_all add: fresh_at_base_permute_iff fresh_def[symmetric] fresh_at_base)
-    apply (subgoal_tac "eqvt app_lst")
-    apply (erule fresh_fun_eqvt_app2)
-    apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev)
-    done
-qed
+termination (eqvt) by lexicographic_order
 
 lemma ltgt_eq_iff[simp]:
   "\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright> \<longleftrightarrow> M = N"
@@ -240,7 +214,7 @@
   "F1 = \<integral>x. (App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> V x))"
   "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> F2 = \<integral>a. \<integral>b. \<integral>c. ((App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (V c \<cdot> V a))) \<cdot> (V c \<cdot> V b))"
   "a \<noteq> b \<Longrightarrow> a \<noteq> x \<Longrightarrow> x \<noteq> b \<Longrightarrow> F3 = \<integral>a. \<integral>b. (App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (V b \<cdot> (V a \<cdot> V x)))))"
-  apply (simp_all add: F1_def F2_def F3_def Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt numeral_eqvt flip_def[symmetric] fresh_at_base)
+  apply (simp_all add: F1_def F2_def F3_def Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt Numeral.eqvt flip_def[symmetric] fresh_at_base)
   apply (smt cx_cy_cz permute_flip_at)+
   done
 
@@ -291,7 +265,7 @@
   "x \<noteq> y \<Longrightarrow> A1 = \<integral>x. \<integral>y. (F1 \<cdot> V x)"
   "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> A2 = \<integral>a. \<integral>b. \<integral>c. (F2 \<cdot> V a \<cdot> V b \<cdot> \<guillemotleft>[V c]\<guillemotright>)"
   "a \<noteq> b \<Longrightarrow> A3 = \<integral>a. \<integral>b. (F3 \<cdot> V a \<cdot> \<guillemotleft>[V b]\<guillemotright>)"
-  apply (simp_all add: Lam_A1_pre Lam_A2_pre Lam_A3_pre Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt numeral_eqvt flip_def[symmetric] fresh_at_base F_eqvt ltgt_eqvt)
+  apply (simp_all add: Lam_A1_pre Lam_A2_pre Lam_A3_pre Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt Numeral.eqvt flip_def[symmetric] fresh_at_base F_eqvt Ltgt.eqvt)
   apply (smt cx_cy_cz permute_flip_at)+
   done