tuned -- avoid recoding properties;

--- a/src/Pure/Concurrent/thread_position.ML	Sat Apr 09 21:42:42 2016 +0200
+++ b/src/Pure/Concurrent/thread_position.ML	Sun Apr 10 17:52:30 2016 +0200
@@ -6,21 +6,22 @@
 
 signature THREAD_POSITION =
 sig
-  val get: unit -> (string * string) list
-  val setmp: (string * string) list -> ('a -> 'b) -> 'a -> 'b
+  type T = {line: int, offset: int, end_offset: int, props: (string * string) list}
+  val none: T
+  val get: unit -> T
+  val setmp: T -> ('a -> 'b) -> 'a -> 'b
 end;
 
 structure Thread_Position: THREAD_POSITION =
 struct
 
-val var = Thread_Data.var () : (string * string) list Thread_Data.var;
+type T = {line: int, offset: int, end_offset: int, props: (string * string) list};
+
+val var = Thread_Data.var () : T Thread_Data.var;
 
-fun get () =
-  (case Thread_Data.get var of
-    NONE => []
-  | SOME props => props);
+val none: T = {line = 0, offset = 0, end_offset = 0, props = []};
 
-fun setmp props f x =
-  Thread_Data.setmp var (if List.null props then NONE else SOME props) f x;
+fun get () = (case Thread_Data.get var of NONE => none | SOME pos => pos);
+fun setmp pos f x = Thread_Data.setmp var (if pos = none then NONE else SOME pos) f x;
 
 end;

--- a/src/Pure/General/position.ML	Sat Apr 09 21:42:42 2016 +0200
+++ b/src/Pure/General/position.ML	Sun Apr 10 17:52:30 2016 +0200
@@ -7,8 +7,8 @@
 signature POSITION =
 sig
   eqtype T
-  val make: {line: int, offset: int, end_offset: int, props: Properties.T} -> T
-  val dest: T -> {line: int, offset: int, end_offset: int, props: Properties.T}
+  val make: Thread_Position.T -> T
+  val dest: T -> Thread_Position.T
   val line_of: T -> int option
   val offset_of: T -> int option
   val end_offset_of: T -> int option
@@ -243,8 +243,8 @@
 
 (* thread data *)
 
-val thread_data = of_properties o Thread_Position.get;
-fun setmp_thread_data pos = Thread_Position.setmp (properties_of pos);
+val thread_data = make o Thread_Position.get;
+fun setmp_thread_data pos = Thread_Position.setmp (dest pos);
 
 fun default pos =
   if pos = none then (false, thread_data ())