operation on embedded sources for Eisbach;

--- 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 *)