--- a/Nominal/Ex/LetRec2.thy	Thu Dec 15 16:20:11 2011 +0000
+++ b/Nominal/Ex/LetRec2.thy	Thu Dec 15 16:20:42 2011 +0000
@@ -22,6 +22,11 @@
 thm trm_assn.eq_iff
 thm trm_assn.supp
 
+ML {*
+@{term Trueprop} ;
+@{const_name HOL.eq}
+*}
+
 thm trm_assn.fv_defs
 thm trm_assn.eq_iff
 thm trm_assn.bn_defs