tuned signature;

--- a/src/Pure/General/position.ML	Tue Sep 06 11:25:27 2011 +0200
+++ b/src/Pure/General/position.ML	Tue Sep 06 19:48:57 2011 +0200
@@ -36,7 +36,7 @@
   val report_text: T -> Markup.T -> string -> unit
   val report: T -> Markup.T -> unit
   type reports = (T * Markup.T) list
-  val reports: reports Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
+  val store_reports: reports Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
   val str_of: T -> string
   type range = T * T
   val no_range: range
@@ -156,8 +156,8 @@
 
 type reports = (T * Markup.T) list;
 
-fun reports _ [] _ _ = ()
-  | reports (r: reports Unsynchronized.ref) ps markup x =
+fun store_reports _ [] _ _ = ()
+  | store_reports (r: reports Unsynchronized.ref) ps markup x =
       let val ms = markup x
       in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
 

--- a/src/Pure/Syntax/syntax_phases.ML	Tue Sep 06 11:25:27 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Sep 06 19:48:57 2011 +0200
@@ -127,7 +127,7 @@
 fun parsetree_to_ast ctxt constrain_pos trf parsetree =
   let
     val reports = Unsynchronized.ref ([]: Position.reports);
-    fun report pos = Position.reports reports [pos];
+    fun report pos = Position.store_reports reports [pos];
 
     fun trans a args =
       (case trf a of
@@ -207,7 +207,7 @@
         val decodeT = typ_of_term (Proof_Context.get_sort ctxt (term_sorts tm));
 
         val reports = Unsynchronized.ref reports0;
-        fun report ps = Position.reports reports ps;
+        fun report ps = Position.store_reports reports ps;
 
         fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
               (case Term_Position.decode_position typ of