| changeset 61814 | 1ca1142e1711 |
| parent 61268 | abe08fb15a12 |
| child 62094 | 7d47cf67516d |
--- a/src/Pure/Isar/bundle.ML Wed Dec 09 16:22:29 2015 +0100 +++ b/src/Pure/Isar/bundle.ML Wed Dec 09 16:36:26 2015 +0100 @@ -35,7 +35,7 @@ type bundle = (thm list * Token.src list) list; fun transform_bundle phi : bundle -> bundle = - map (fn (fact, atts) => (Morphism.fact phi fact, map (Token.transform_src phi) atts)); + map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts)); structure Data = Generic_Data (