equal
deleted
inserted
replaced
619 in map (expand_eta thy k) thms end; |
619 in map (expand_eta thy k) thms end; |
620 |
620 |
621 fun mk_desymbolization pre post mk vs = |
621 fun mk_desymbolization pre post mk vs = |
622 let |
622 let |
623 val names = map (pre o fst o fst) vs |
623 val names = map (pre o fst o fst) vs |
624 |> map (Name.desymbolize false) |
624 |> map (Name.desymbolize (SOME false)) |
625 |> Name.variant_list [] |
625 |> Name.variant_list [] |
626 |> map post; |
626 |> map post; |
627 in map_filter (fn (((v, i), x), v') => |
627 in map_filter (fn (((v, i), x), v') => |
628 if v = v' andalso i = 0 then NONE |
628 if v = v' andalso i = 0 then NONE |
629 else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names) |
629 else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names) |