diff -r ade2f8fcf8e8 -r 51ef8a3cb6ef Nominal/Ex/LetRec2.thy
--- 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