# HG changeset patch
# User wenzelm
# Date 1427970270 -7200
# Node ID fdf6957f86355350c32961c0e951a68207438605
# Parent  6c0f6249069950d8fb7f952de851cc830cfeb59c
operation on embedded sources for Eisbach;

diff -r 6c0f62490699 -r fdf6957f8635 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu Apr 02 11:41:14 2015 +0200
+++ b/src/Pure/Isar/token.ML	Thu Apr 02 12:24:30 2015 +0200
@@ -72,6 +72,7 @@
   val get_value: T -> value option
   val map_value: (value -> value) -> T -> T
   val reports_of_value: T -> Position.report list
+  val map_values: (value -> value) -> src -> src
   val declare_maxidx: T -> Proof.context -> Proof.context
   val declare_maxidx_src: src -> Proof.context -> Proof.context
   val transform: morphism -> T -> T
@@ -403,6 +404,9 @@
       end
   | _ => []);
 
+fun map_values f =
+  (map_args o map_value) (fn Source src => Source (map_values f src) | x => f x);
+
 
 (* maxidx *)