--- a/Nominal/Ex/SingleLet.thy	Sun Aug 22 12:36:53 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sun Aug 22 14:02:49 2010 +0800
@@ -42,78 +42,68 @@
 thm bn_eqvt
 thm size_eqvt
 
+ML {* lift_thm *}
+
+
 ML {*
-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
+  val _ = timeit (fn () => map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms distinct})
+*}
+
+ML {* 
+  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 _ = timeit (fn () => map (lifted @{context} [@{typ trm}, @{typ assg}]) @{thms distinct})
-*}
-
-ML {* 
-  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_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms fv_defs}
+  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_p = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms perm_simps}
+  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 @{context} [@{typ trm}, @{typ assg}]) @{thms perm_laws}
+  val thms_p = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms perm_simps}
 *}
 
 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]}
+  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms perm_laws}
+*}
+
+ML {*
+  val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
+    prod.cases}
 *}
 
 ML {*
- 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]}
+ val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}] simps)  @{thms eq_iff}
 *}
 
 ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms bn_defs}
+ val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}] simps) @{thms eq_iff_simps}
 *}
 
 ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms bn_eqvt}
+  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms bn_defs}
 *}
 
 ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms fv_eqvt}
+  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms bn_eqvt}
 *}
 
 ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms size_eqvt}
+  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms fv_eqvt}
+*}
+
+ML {*
+  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms size_eqvt}
 *}