diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/Lambda.thy	Mon May 19 16:45:46 2014 +0100
@@ -86,7 +86,7 @@
 apply(all_trivials)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 thm is_app_def
 thm is_app.eqvt
@@ -106,7 +106,7 @@
 apply(simp_all)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 nominal_function 
   rand :: "lam \<Rightarrow> lam option"
@@ -121,7 +121,7 @@
 apply(simp_all)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 nominal_function 
   is_eta_nf :: "lam \<Rightarrow> bool"
@@ -142,7 +142,7 @@
 apply(simp add: eqvt_at_def conj_eqvt)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 nominal_datatype path = Left | Right | In
 
@@ -181,7 +181,7 @@
 apply(simp add: perm_supp_eq)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma var_pos1:
   assumes "atom y \<notin> supp t"
@@ -227,7 +227,7 @@
   apply(simp add: fresh_star_Pair perm_supp_eq)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 
 section {* free name function *}
@@ -252,7 +252,7 @@
 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 text {* a small test lemma *}
 lemma shows "supp t = set (frees_lst t)"
@@ -280,7 +280,7 @@
   apply(simp add: Diff_eqvt eqvt_at_def)
   done
 
-termination (eqvt) 
+nominal_termination (eqvt) 
   by lexicographic_order
 
 lemma "frees_set t = supp t"
@@ -303,7 +303,7 @@
   apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
   
 thm height.simps
@@ -338,7 +338,7 @@
   apply(simp add: fresh_star_Pair perm_supp_eq)
 done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 thm subst.eqvt
@@ -530,7 +530,7 @@
   apply(simp add: fresh_star_Pair perm_supp_eq)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 
@@ -557,7 +557,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 
@@ -591,7 +591,7 @@
   apply(simp add: fresh_star_Pair perm_supp_eq)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 section {* De Bruijn Terms *}
@@ -649,7 +649,7 @@
   apply(simp add: fresh_star_Pair perm_supp_eq)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 lemma transdb_eqvt[eqvt]:
@@ -722,7 +722,7 @@
 
 
 (* a small test
-termination (eqvt) sorry
+nominal_termination (eqvt) sorry
 
 lemma 
   assumes "x \<noteq> y"
@@ -774,7 +774,7 @@
   apply (simp add: eqvt_def permute_fun_app_eq)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order