--- a/Nominal/Ex/CoreHaskell.thy	Sat Aug 21 20:07:52 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Sun Aug 22 11:00:53 2010 +0800
@@ -106,49 +106,82 @@
 *}
 
 ML {*
-  val thms_d = map (lift_thm qtys @{context}) @{thms distinct}
-*}
-
-ML {* 
-  val thms_i = map (lift_thm qtys @{context}) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts}
+fun lifted ctxt qtys rthm =
+let
+  (* When the theorem is atomized, eta redexes are contracted,
+     so we do it both in the original theorem *)
+  val rthm' = Drule.eta_contraction_rule rthm
+  val ((_, [rthm'']), ctxt') = Variable.import false [rthm'] ctxt
+  val goal = Quotient_Term.derive_qtrm ctxt' qtys (prop_of rthm'')
+in
+  Goal.prove ctxt' [] [] goal (K (Quotient_Tacs.lift_tac ctxt' [rthm'] 1))
+  |> singleton (ProofContext.export ctxt' ctxt)
+end
 *}
 
 ML {*
-  val thms_f = map (lift_thm qtys @{context}) @{thms fv_defs}
+fun lifted2 ctxt qtys rthms =
+let
+  (* When the theorem is atomized, eta redexes are contracted,
+     so we do it both in the original theorem *)
+  val rthms' = map Drule.eta_contraction_rule rthms
+  val ((_, rthms''), ctxt') = Variable.import false rthms' ctxt
+  val goals = map (Quotient_Term.derive_qtrm ctxt' qtys o prop_of) rthms''
+in
+  Goal.prove_multi ctxt' [] [] goals (K (Quotient_Tacs.lift_tac ctxt' rthms' 1))
+  |> ProofContext.export ctxt' ctxt
+end
+*}
+
+ML {*
+  val _ = timeit (fn () => map (lifted @{context} qtys) @{thms distinct})
+*}
+
+ML {*
+  val _ = timeit (fn () => lifted2 @{context} qtys @{thms distinct})
+*}
+
+
+ML {* 
+  val thms_i = map (lift_thm @{context} qtys) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts}
+*}
+
+ML {*
+  val thms_f = map (lift_thm @{context} qtys) @{thms fv_defs}
 *}
 
 ML {* 
-  val thms_i = map (lift_thm qtys @{context}) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98)}
+  val thms_i = map (lift_thm @{context} qtys) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98)}
 *}
 
 ML {*
-  val thms_p = map (lift_thm qtys @{context}) @{thms perm_simps}
+  val thms_p = map (lift_thm @{context} qtys) @{thms perm_simps}
 *}
 
 ML {*
-  val thms_f = map (lift_thm qtys @{context}) @{thms perm_laws}
+  val thms_f = map (lift_thm @{context} qtys) @{thms perm_laws}
 *}
 
 ML {*
- val thms_e = map (lift_thm qtys @{context}) 
+ val thms_e = map (lift_thm @{context} qtys) 
    @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
     prod.cases]}
 *}
 
 ML {*
-  val thms_f = map (lift_thm qtys @{context}) @{thms bn_defs}
+  val thms_f = map (lift_thm @{context} qtys) @{thms bn_defs}
 *}
 
 ML {*
-  val thms_f = map (lift_thm qtys @{context}) @{thms bn_eqvt}
+  val thms_f = map (lift_thm @{context} qtys) @{thms bn_eqvt}
 *}
 
 ML {*
-  val thms_f = map (lift_thm qtys @{context}) @{thms fv_eqvt}
+  val thms_f = map (lift_thm @{context} qtys) @{thms fv_eqvt}
 *}
 
 ML {*
-  val thms_f = map (lift_thm qtys @{context}) @{thms size_eqvt}
+  val thms_f = map (lift_thm @{context} qtys) @{thms size_eqvt}
 *}