109   val thms_d = map (lift_thm qtys @{context}) @{thms distinct}

   109 fun lifted ctxt qtys rthm =

   110 *}

   110 let

   111   (* When the theorem is atomized, eta redexes are contracted,

   112      so we do it both in the original theorem *)

   113   val rthm' = Drule.eta_contraction_rule rthm

   114   val ((_, [rthm'']), ctxt') = Variable.import false [rthm'] ctxt

   115   val goal = Quotient_Term.derive_qtrm ctxt' qtys (prop_of rthm'')

   116 in

   117   Goal.prove ctxt' [] [] goal (K (Quotient_Tacs.lift_tac ctxt' [rthm'] 1))

   118   |> singleton (ProofContext.export ctxt' ctxt)

   119 end

   120 *}

   121 

   122 ML {*

   123 fun lifted2 ctxt qtys rthms =

   124 let

   125   (* When the theorem is atomized, eta redexes are contracted,

   126      so we do it both in the original theorem *)

   127   val rthms' = map Drule.eta_contraction_rule rthms

   128   val ((_, rthms''), ctxt') = Variable.import false rthms' ctxt

   129   val goals = map (Quotient_Term.derive_qtrm ctxt' qtys o prop_of) rthms''

   130 in

   131   Goal.prove_multi ctxt' [] [] goals (K (Quotient_Tacs.lift_tac ctxt' rthms' 1))

   132   |> ProofContext.export ctxt' ctxt

   133 end

   134 *}

   135 

   136 ML {*

   137   val _ = timeit (fn () => map (lifted @{context} qtys) @{thms distinct})

   138 *}

   139 

   140 ML {*

   141   val _ = timeit (fn () => lifted2 @{context} qtys @{thms distinct})

   142 *}

   143 

   113   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}

   146   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}

   114 *}

   147 *}

   115 

   148 

   116 ML {*

   149 ML {*

   117   val thms_f = map (lift_thm qtys @{context}) @{thms fv_defs}

   150   val thms_f = map (lift_thm @{context} qtys) @{thms fv_defs}

   121   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)}

   154   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)}

   122 *}

   155 *}

   123 

   156 

   124 ML {*

   157 ML {*

   125   val thms_p = map (lift_thm qtys @{context}) @{thms perm_simps}

   158   val thms_p = map (lift_thm @{context} qtys) @{thms perm_simps}

   126 *}

   159 *}

   127 

   160 

   128 ML {*

   161 ML {*

   129   val thms_f = map (lift_thm qtys @{context}) @{thms perm_laws}

   162   val thms_f = map (lift_thm @{context} qtys) @{thms perm_laws}

   130 *}

   163 *}

   131 

   164 

   132 ML {*

   165 ML {*

   133  val thms_e = map (lift_thm qtys @{context}) 

   166  val thms_e = map (lift_thm @{context} qtys) 

   139   val thms_f = map (lift_thm qtys @{context}) @{thms bn_defs}

   172   val thms_f = map (lift_thm @{context} qtys) @{thms bn_defs}

   140 *}

   173 *}

   141 

   174 

   142 ML {*

   175 ML {*

   143   val thms_f = map (lift_thm qtys @{context}) @{thms bn_eqvt}

   176   val thms_f = map (lift_thm @{context} qtys) @{thms bn_eqvt}

   144 *}

   177 *}

   145 

   178 

   146 ML {*

   179 ML {*

   147   val thms_f = map (lift_thm qtys @{context}) @{thms fv_eqvt}

   180   val thms_f = map (lift_thm @{context} qtys) @{thms fv_eqvt}

   148 *}

   181 *}

   149 

   182 

   150 ML {*

   183 ML {*

   151   val thms_f = map (lift_thm qtys @{context}) @{thms size_eqvt}

   184   val thms_f = map (lift_thm @{context} qtys) @{thms size_eqvt}