equal
deleted
inserted
replaced
575 (* Theorems *) |
575 (* Theorems *) |
576 |
576 |
577 local |
577 local |
578 |
578 |
579 val trim_fact = map Thm.trim_context; |
579 val trim_fact = map Thm.trim_context; |
580 val trim_srcs = (map o map o Token.map_facts) trim_fact; |
580 val trim_srcs = (map o map o Token.map_facts) (K trim_fact); |
581 |
581 |
582 fun trim_context_facts facts = facts |> map (fn ((b, atts), args) => |
582 fun trim_context_facts facts = facts |> map (fn ((b, atts), args) => |
583 ((b, trim_srcs atts), map (fn (a, more_atts) => (trim_fact a, trim_srcs more_atts)) args)); |
583 ((b, trim_srcs atts), map (fn (a, more_atts) => (trim_fact a, trim_srcs more_atts)) args)); |
584 |
584 |
585 in |
585 in |