src/Pure/Isar/token.ML

--- a/src/Pure/Isar/token.ML	Mon Feb 24 00:04:48 2014 +0100
+++ b/src/Pure/Isar/token.ML	Mon Feb 24 10:17:29 2014 +0100
@@ -16,10 +16,8 @@
     Attribute of morphism -> attribute | Files of file Exn.result list
   type T
   val str_of_kind: kind -> string
-  val position_of: T -> Position.T
-  val end_position_of: T -> Position.T
+  val pos_of: T -> Position.T
   val position_range_of: T list -> Position.range
-  val pos_of: T -> string
   val eof: T
   val is_eof: T -> bool
   val not_eof: T -> bool
@@ -130,13 +128,11 @@
 
 (* position *)
 
-fun position_of (Token ((_, (pos, _)), _, _)) = pos;
-fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
+fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
+fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
 
 fun position_range_of [] = Position.no_range
-  | position_range_of toks = (position_of (hd toks), end_position_of (List.last toks));
-
-val pos_of = Position.here o position_of;
+  | position_range_of toks = (pos_of (hd toks), end_pos_of (List.last toks));
 
 
 (* control tokens *)
@@ -153,7 +149,7 @@
   | not_sync _ = true;
 
 val stopper =
-  Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
+  Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
 
 
 (* kind of token *)
@@ -251,8 +247,7 @@
 
 fun put_files [] tok = tok
   | put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
-  | put_files _ tok =
-      raise Fail ("Cannot put inlined files here" ^ Position.here (position_of tok));
+  | put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok));
 
 
 (* access values *)