--- a/Nominal/Ex/Lambda.thy	Sun Jan 09 01:17:44 2011 +0000
+++ b/Nominal/Ex/Lambda.thy	Sun Jan 09 04:28:24 2011 +0000
@@ -22,6 +22,16 @@
 thm lam.fv_bn_eqvt
 thm lam.size_eqvt
 
+definition
+ "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"
+
+function
+  depth :: "lam \<Rightarrow> nat"
+where
+  "depth (Var x) = 1"
+| "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
+| "depth (Lam x t) = (depth t) + 1"
+oops
 
 section {* Matching *}