src/Pure/Isar/method.ML
changeset 76804 3e8340fcaa16
parent 74887 56247fdb8bbb
child 77908 a6bd716a6124
--- a/src/Pure/Isar/method.ML	Wed Dec 28 16:02:12 2022 +0100
+++ b/src/Pure/Isar/method.ML	Wed Dec 28 16:13:08 2022 +0100
@@ -667,7 +667,7 @@
       (keyword_positions text);
 
 fun report text_range =
-  if Context_Position.pide_reports ()
+  if Context_Position.reports_enabled0 ()
   then Position.reports (reports_of text_range) else ();
 
 end;