equal
deleted
inserted
replaced
289 |
289 |
290 |
290 |
291 fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys = |
291 fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys = |
292 let |
292 let |
293 (* proper import of type-variables does not work, |
293 (* proper import of type-variables does not work, |
294 since ther are replaced by new variables, messing |
294 since then they are replaced by new variables, messing |
295 up the ty_term assoc list *) |
295 up the ty_term assoc list *) |
296 val distinct_thms' = map Thm.legacy_freezeT distinct_thms |
296 val distinct_thms' = map Thm.legacy_freezeT distinct_thms |
297 val ty_trm_assoc = alpha_tys ~~ alpha_trms |
297 val ty_trm_assoc = alpha_tys ~~ alpha_trms |
298 |
298 |
299 fun mk_alpha_distinct distinct_trm = |
299 fun mk_alpha_distinct distinct_trm = |