Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Syntax/syntax_phases.ML
changeset 44735 66862d02678c
parent 44564 96ba83710946
child 44736 c2a3f1c84179 
--- 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
isabelle