src/Pure/General/name_space.ML
changeset 71674 48ff625687f5
parent 71257 b1f3e86a4745
child 72053 4ed33ea8d957
--- a/src/Pure/General/name_space.ML	Fri Apr 03 12:45:14 2020 +0200
+++ b/src/Pure/General/name_space.ML	Fri Apr 03 13:51:56 2020 +0200
@@ -575,7 +575,7 @@
 fun check context table (xname, pos) =
   let
     val ((name, reports), x) = check_reports context table (xname, [pos]);
-    val _ = Position.reports reports;
+    val _ = Context_Position.reports_generic context reports;
   in (name, x) end;
 
 fun defined (Table (_, tab)) name = Change_Table.defined tab name;