--- a/Nominal/Ex/LetRec.thy	Mon Jul 18 17:40:13 2011 +0100
+++ b/Nominal/Ex/LetRec.thy	Tue Jul 19 01:40:36 2011 +0100
@@ -59,6 +59,16 @@
   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
+*}
+
+
 thm height_trm_def height_bp_def
 
 termination (eqvt) by lexicographic_order