--- a/Nominal/Ex/LetRec.thy	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/Ex/LetRec.thy	Mon Jul 18 17:40:13 2011 +0100
@@ -59,7 +59,9 @@
   apply (simp add: permute_fun_def)
   done
 
-termination by lexicographic_order
+thm height_trm_def height_bp_def
+
+termination (eqvt) by lexicographic_order
 
 end