107 

   107 

   108 

   108 

   109 ML {*

   109 ML {*

   110   val _ = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct})

   110   val _ = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct})

   111 *}

   111 *}

   113 

   112 

   114 ML {* 

   113 ML {* 

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

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

   116 *}

   115 *}

   117 

   116