diff -r 66ae73fd66c0 -r 29ebbe56f450 Nominal/Ex/CoreHaskell.thy
--- a/Nominal/Ex/CoreHaskell.thy	Tue Aug 17 06:39:27 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Tue Aug 17 06:50:49 2010 +0800
@@ -135,6 +135,10 @@
     prod.cases]}
 *}
 
+ML {*
+  val thms_f = map (lift_thm qtys @{context}) @{thms bn_defs}
+*}
+
 
 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]