equal
deleted
inserted
replaced
495 |
495 |
496 fun burrow_ids f ithms = |
496 fun burrow_ids f ithms = |
497 let |
497 let |
498 val (is, thms) = split_list ithms |
498 val (is, thms) = split_list ithms |
499 val (thms', extra_thms) = f thms |
499 val (thms', extra_thms) = f thms |
500 in (is ~~ thms') @ map (pair ~1) extra_thms end |
500 in (is ~~ thms') @ tag_list (length is) extra_thms end |
501 |
501 |
502 fun unfold2 ctxt ithms = |
502 fun unfold2 ctxt ithms = |
503 ithms |
503 ithms |
504 |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt))) |
504 |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt))) |
505 |> burrow_ids add_nat_embedding |
505 |> burrow_ids add_nat_embedding |