--- a/Nominal/Ex/Lambda.thy	Mon Jul 18 17:40:13 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Jul 19 01:40:36 2011 +0100
@@ -46,13 +46,10 @@
 termination (eqvt) by lexicographic_order
 
 ML {*
-Item_Net.content; 
-Nominal_Function_Common.get_function
+Item_Net.content (Nominal_Function_Common.get_function @{context})
 *}
 
-ML {*
-Item_Net.content (Nominal_Function_Common.get_function @{context})
-*}
+thm is_app_def
 
 
 lemma [eqvt]:
@@ -165,6 +162,11 @@
 apply(rule refl)
 done
 
+thm inl_eqvt
+thm var_pos_def
+
+thm fun_eq_iff
+
 termination (eqvt) by lexicographic_order
 
 lemma var_pos1: