--- a/Nominal/Ex/CoreHaskell.thy	Sun Aug 22 12:36:53 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Sun Aug 22 14:02:49 2010 +0800
@@ -105,83 +105,55 @@
               @{typ tvars}, @{typ cvars}]
 *}
 
-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
-*}
 
 ML {*
-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})
+  val _ = timeit (fn () => map (lift_thm @{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}
+  val _ = timeit (fn () => 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.induct})
 *}
 
 ML {*
-  val thms_f = map (lift_thm @{context} qtys) @{thms fv_defs}
+  val thms_f = map (lift_thm @{context} qtys []) @{thms fv_defs}
 *}
 
 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.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 @{context} qtys) @{thms perm_simps}
+  val thms_p = map (lift_thm @{context} qtys []) @{thms perm_simps}
 *}
 
 ML {*
-  val thms_f = map (lift_thm @{context} qtys) @{thms perm_laws}
+  val thms_f = map (lift_thm @{context} qtys []) @{thms perm_laws}
 *}
 
 ML {*
- 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]}
+  val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
+    prod.cases}
 *}
 
 ML {*
-  val thms_f = map (lift_thm @{context} qtys) @{thms bn_defs}
+ val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff}
 *}
 
 ML {*
-  val thms_f = map (lift_thm @{context} qtys) @{thms bn_eqvt}
+  val thms_f = map (lift_thm @{context} qtys []) @{thms bn_defs}
 *}
 
 ML {*
-  val thms_f = map (lift_thm @{context} qtys) @{thms fv_eqvt}
+  val thms_f = map (lift_thm @{context} qtys []) @{thms bn_eqvt}
 *}
 
 ML {*
-  val thms_f = map (lift_thm @{context} qtys) @{thms size_eqvt}
+  val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt}
+*}
+
+ML {*
+  val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt}
 *}