--- a/src/Pure/Isar/proof_context.ML Fri Apr 03 13:51:56 2020 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Apr 03 17:35:10 2020 +0200
@@ -792,7 +792,7 @@
fun check_tfree ctxt v =
let
val (sorting_report, [TFree a]) = prepare_sortsT ctxt [TFree v];
- val _ = if Context_Position.is_visible ctxt then Output.report sorting_report else ();
+ val _ = if Context_Position.reports_enabled ctxt then Output.report sorting_report else ();
in a end;
end;
@@ -1103,7 +1103,7 @@
let
val ([x], ctxt') = Variable.add_fixes_binding [Binding.reset_pos b] ctxt;
val mx' = Mixfix.reset_pos mx;
- val _ = add_syntax [(x, T, if Context_Position.is_visible ctxt then mx else mx')] ctxt';
+ val _ = add_syntax [(x, T, if Context_Position.reports_enabled ctxt then mx else mx')] ctxt';
in mx' end;
fun prep_var prep_typ internal (b, raw_T, mx) ctxt =