# HG changeset patch
# User wenzelm
# Date 1394461829 -3600
# Node ID 422024102d9d8cb5d1dc39b9785d20848a9e185e
# Parent  25889f5c39a8a6513dce381604a885224b7ab7c9
tuned signature;

diff -r 25889f5c39a8 -r 422024102d9d 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;
diff -r 25889f5c39a8 -r 422024102d9d src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Mar 10 15:20:41 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Mar 10 15:30:29 2014 +0100
@@ -529,7 +529,7 @@
 
 (* default output *)
 
-val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src;
+val str_of_source = space_implode " " o Args.unparse_src;
 
 fun maybe_pretty_source pretty ctxt src xs =
   map (pretty ctxt) xs  (*always pretty in order to exhibit errors!*)