--- a/Nominal/Ex/Lambda.thy	Tue Jan 18 21:28:07 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Wed Jan 19 07:06:47 2011 +0100
@@ -20,11 +20,11 @@
 thm lam.size_eqvt
 
 nominal_primrec
-  depth :: "lam \<Rightarrow> nat"
+  height :: "lam \<Rightarrow> int"
 where
-  "depth (Var x) = 1"
-| "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
-| "depth (Lam x t) = (depth t) + 1"
+  "height (Var x) = 1"
+| "height (App t1 t2) = (max (height t1) (height t2)) + 1"
+| "height (Lam x t) = (height t) + 1"
 apply(rule_tac y="x" in lam.exhaust)
 apply(simp_all)[3]
 apply(simp_all only: lam.distinct)
@@ -159,6 +159,11 @@
 apply(auto simp add: fresh_star_def fresh_Pair)[1]
 done
 
+termination
+  apply(relation "measure (\<lambda>(t,_,_). size t)")
+  apply(simp_all add: lam.size)
+  done
+
 nominal_datatype ln = 
   LNBnd nat
 | LNVar name