diff -r 29ebbe56f450 -r 428d9cb9a243 Nominal/Ex/CoreHaskell.thy
--- a/Nominal/Ex/CoreHaskell.thy	Tue Aug 17 06:50:49 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Tue Aug 17 07:11:45 2010 +0800
@@ -139,6 +139,20 @@
   val thms_f = map (lift_thm qtys @{context}) @{thms bn_defs}
 *}
 
+ML {*
+  val thms_f = map (lift_thm qtys @{context}) @{thms bn_eqvt}
+*}
+
+ML {*
+  val thms_f = map (lift_thm qtys @{context}) @{thms fv_eqvt}
+*}
+
+ML {*
+  val thms_f = map (lift_thm qtys @{context}) @{thms size_eqvt}
+*}
+
+
+
 
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]