src/Pure/Isar/args.ML

--- a/src/Pure/Isar/args.ML	Mon Mar 10 15:20:41 2014 +0100
+++ b/src/Pure/Isar/args.ML	Mon Mar 10 15:30:29 2014 +0100
@@ -10,6 +10,7 @@
   type src
   val src: (string * Token.T list) * Position.T -> src
   val dest_src: src -> (string * Token.T list) * Position.T
+  val unparse_src: src -> string list
   val pretty_src: (string -> Pretty.T) -> Proof.context -> src -> Pretty.T
   val map_name: (string -> string) -> src -> src
   val transform_values: morphism -> src -> src
@@ -79,6 +80,8 @@
 val src = Src;
 fun dest_src (Src src) = src;
 
+fun unparse_src (Src ((_, toks), _)) = map Token.unparse toks;
+
 fun pretty_src pretty_name ctxt src =
   let
     val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;