| changeset 61820 | e65344e3eeb5 |
| parent 61814 | 1ca1142e1711 |
| child 63029 | 8b830d2bf94c |
--- a/src/Pure/Isar/locale.ML Wed Dec 09 20:58:09 2015 +0100 +++ b/src/Pure/Isar/locale.ML Wed Dec 09 21:10:45 2015 +0100 @@ -577,7 +577,7 @@ local val trim_fact = map Thm.trim_context; -val trim_srcs = (map o map o Token.map_facts) trim_fact; +val trim_srcs = (map o map o Token.map_facts) (K trim_fact); fun trim_context_facts facts = facts |> map (fn ((b, atts), args) => ((b, trim_srcs atts), map (fn (a, more_atts) => (trim_fact a, trim_srcs more_atts)) args));