--- a/Nominal/Ex/LetRec.thy	Tue Jul 19 01:40:36 2011 +0100
+++ b/Nominal/Ex/LetRec.thy	Tue Jul 19 02:30:05 2011 +0100
@@ -59,19 +59,10 @@
   apply (simp add: permute_fun_def)
   done
 
-ML {*
-let
-  val [t1, t2] = Item_Net.content (Nominal_Function_Common.get_function @{context})
-in
-  (#eqvts (snd t1),
-   #eqvts (snd t2))
-end
-*}
+termination (eqvt) by lexicographic_order
 
+thm height_trm_height_bp.eqvt
 
-thm height_trm_def height_bp_def
-
-termination (eqvt) by lexicographic_order
 
 end