--- a/src/Pure/Isar/bundle.ML Fri Apr 25 11:22:25 2025 +0200
+++ b/src/Pure/Isar/bundle.ML Fri Apr 25 11:34:29 2025 +0200
@@ -110,8 +110,10 @@
end;
fun print_bundles verbose ctxt =
- Pretty.writeln (Pretty.chunks
- (map (pretty_bundle ctxt) (Name_Space.markup_table verbose ctxt (get_all ctxt))));
+ Name_Space.markup_table verbose ctxt (get_all ctxt)
+ |> map (pretty_bundle ctxt)
+ |> Pretty.chunks
+ |> Pretty.writeln;
--- a/src/Pure/Isar/code.ML Fri Apr 25 11:22:25 2025 +0200
+++ b/src/Pure/Isar/code.ML Fri Apr 25 11:34:29 2025 +0200
@@ -1111,8 +1111,9 @@
fun apply_functrans ctxt functrans =
let
- fun trace_eqns s eqns = (Pretty.writeln o Pretty.chunks)
- (Pretty.str s :: map (Thm.pretty_thm ctxt o fst) eqns);
+ fun trace_eqns s eqns =
+ Pretty.writeln (Pretty.chunks
+ (Pretty.str s :: map (Thm.pretty_thm ctxt o fst) eqns));
val tracing = if Config.get ctxt simp_trace then trace_eqns else (K o K) ();
in
tap (tracing "before function transformation")