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;