--- 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]

--- a/Nominal/Ex/SingleLet.thy	Tue Aug 17 06:39:27 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Tue Aug 17 06:50:49 2010 +0800
@@ -29,10 +29,9 @@
 thm perm_simps
 thm perm_laws
 thm trm_raw_assg_raw.size(9 - 16)
-
-(* cannot lift yet *)
 thm eq_iff
 thm eq_iff_simps
+
 (* bn / eqvt lemmas for fv / fv_bn / bn *)
 
 ML {*
@@ -59,18 +58,21 @@
   val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws}
 *}
 
-
-section {* NOT *} 
-
 ML {*
  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) 
    @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
     prod.cases]}
 *}
 
-
+ML {*
+ val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) 
+   @{thms eq_iff_simps[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
+    prod.cases]}
+*}
 
-
+ML {*
+  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms bn_defs}
+*}
 
 thm perm_defs
 thm perm_simps

--- a/Nominal/NewParser.thy	Tue Aug 17 06:39:27 2010 +0800
+++ b/Nominal/NewParser.thy	Tue Aug 17 06:50:49 2010 +0800
@@ -341,7 +341,7 @@
 
   (* definition of raw fv_functions *)
   val _ = warning "Definition of raw fv-functions";
-  val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
+  val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) =
     if get_STEPS lthy3 > 2 
     then raw_bn_decls raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs 
       (raw_inject_thms @ raw_distinct_thms) lthy3
@@ -377,7 +377,7 @@
   val _ = warning "Proving equivariance";
   val bn_eqvt = 
     if get_STEPS lthy > 6
-    then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_simps) lthy4
+    then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_defs @ raw_perm_simps) lthy4
     else raise TEST lthy4
 
   (* noting the bn_eqvt lemmas in a temprorary theory *)
@@ -439,7 +439,7 @@
   
   (* respectfulness proofs *)
   val raw_funs_rsp_aux = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
-    raw_bns raw_fv_bns alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6
+    raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6
   val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux
 
   val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct 
@@ -534,6 +534,7 @@
      ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff)
      ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) 
      ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) 
+     ||>> Local_Theory.note ((@{binding "bn_defs"}, []), raw_bn_defs) 
      ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) 
      ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) 
      ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
@@ -554,7 +555,7 @@
   val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
   val bns = raw_bns ~~ bn_nos;
 
-  val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8;
+  val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_defs (map fst bns) lthy8;
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
        resolve_tac bns_rsp_pre' 1)) bns lthy8;
@@ -622,7 +623,7 @@
   val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
   val q_fv = map (lift_thm qtys lthy15) raw_fv_defs;
   val lthy16 = note_simp_suffix "fv" q_fv lthy15;
-  val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
+  val q_bn = map (lift_thm qtys lthy16) raw_bn_defs;
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = warning "Lifting eq-iff";
   (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)