--- a/Nominal/Ex/Lambda.thy	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Mon Jul 18 17:40:13 2011 +0100
@@ -43,7 +43,17 @@
 apply(all_trivials)
 done
 
-termination by lexicographic_order
+termination (eqvt) by lexicographic_order
+
+ML {*
+Item_Net.content; 
+Nominal_Function_Common.get_function
+*}
+
+ML {*
+Item_Net.content (Nominal_Function_Common.get_function @{context})
+*}
+
 
 lemma [eqvt]:
   shows "(p \<bullet> (is_app t)) = is_app (p \<bullet> t)"
@@ -65,7 +75,7 @@
 apply(simp_all)
 done
 
-termination by lexicographic_order
+termination (eqvt) by lexicographic_order
 
 lemma [eqvt]:
   shows "(p \<bullet> (rator t)) = rator (p \<bullet> t)"
@@ -87,7 +97,7 @@
 apply(simp_all)
 done
 
-termination by lexicographic_order
+termination (eqvt) by lexicographic_order
 
 lemma [eqvt]:
   shows "(p \<bullet> (rand t)) = rand (p \<bullet> t)"
@@ -118,7 +128,7 @@
 apply(rule refl)
 done
 
-termination by lexicographic_order
+termination (eqvt) by lexicographic_order
 
 nominal_datatype path = Left | Right | In
 
@@ -155,7 +165,7 @@
 apply(rule refl)
 done
 
-termination by lexicographic_order
+termination (eqvt) by lexicographic_order
 
 lemma var_pos1:
   assumes "atom y \<notin> supp t"
@@ -195,7 +205,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 done
 
-termination by lexicographic_order
+termination (eqvt) by lexicographic_order
 
 
 section {* free name function *}
@@ -221,7 +231,7 @@
 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt)
 done
 
-termination by lexicographic_order
+termination (eqvt) by lexicographic_order
 
 text {* a small test lemma *}
 lemma shows "supp t = set (frees_lst t)"
@@ -249,7 +259,7 @@
   apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl)
   done
 
-termination 
+termination (eqvt) 
   by lexicographic_order
 
 lemma "frees_set t = supp t"
@@ -272,7 +282,7 @@
   apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
   done
 
-termination
+termination (eqvt)
   by lexicographic_order
   
 thm height.simps
@@ -300,7 +310,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 done
 
-termination
+termination (eqvt)
   by lexicographic_order
 
 lemma subst_eqvt[eqvt]:
@@ -486,7 +496,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   done
 
-termination
+termination (eqvt)
   by lexicographic_order
 
 
@@ -513,7 +523,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   done
 
-termination
+termination (eqvt)
   by lexicographic_order
 
 
@@ -543,7 +553,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   done
 
-termination
+termination (eqvt)
   by lexicographic_order
 
 section {* De Bruijn Terms *}
@@ -594,7 +604,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq eqvts eqvts_raw)+
   done
 
-termination
+termination (eqvt)
   by lexicographic_order
 
 lemma transdb_eqvt[eqvt]:
@@ -665,7 +675,7 @@
 
 
 (* a small test
-termination sorry
+termination (eqvt) sorry
 
 lemma 
   assumes "x \<noteq> y"
@@ -719,7 +729,7 @@
   apply (simp add: eqvt_def permute_fun_app_eq)
   done
 
-termination
+termination (eqvt)
   by lexicographic_order