--- a/Nominal/Ex/SingleLet.thy	Sat Aug 21 20:07:52 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sun Aug 22 11:00:53 2010 +0800
@@ -23,8 +23,6 @@
   "bn (As x y t) = {atom x}"
 
 
-
-
 ML {* Function.prove_termination *}
 
 text {* can lift *}
@@ -44,65 +42,78 @@
 thm bn_eqvt
 thm size_eqvt
 
-
 ML {*
-  val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct}
-*}
-
-ML {* 
-  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts}
-*}
-
-ML {* 
-  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw.exhaust}
-*}
-
-ML {* 
-  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms assg_raw.exhaust}
+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 [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs}
+  val _ = timeit (fn () => map (lifted @{context} [@{typ trm}, @{typ assg}]) @{thms distinct})
 *}
 
 ML {* 
-  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)}
+  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms trm_raw_assg_raw.inducts}
+*}
+
+ML {* 
+  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms trm_raw.exhaust}
+*}
+
+ML {* 
+  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms assg_raw.exhaust}
 *}
 
 ML {*
-  val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps}
+  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms fv_defs}
+*}
+
+ML {* 
+  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms trm_raw_assg_raw.size(9 - 16)}
 *}
 
 ML {*
-  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws}
+  val thms_p = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms perm_simps}
 *}
 
 ML {*
- val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) 
+  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms perm_laws}
+*}
+
+ML {*
+ val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) 
    @{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}) 
+ val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) 
    @{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}
+  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms bn_defs}
 *}
 
 ML {*
-  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms bn_eqvt}
+  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms bn_eqvt}
 *}
 
 ML {*
-  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_eqvt}
+  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms fv_eqvt}
 *}
 
 ML {*
-  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms size_eqvt}
+  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms size_eqvt}
 *}