tuned;

--- a/src/Pure/System/process_result.ML	Mon Feb 22 16:54:33 2021 +0100
+++ b/src/Pure/System/process_result.ML	Mon Feb 22 16:58:56 2021 +0100
@@ -41,6 +41,8 @@
 val err_lines = #err_lines o rep;
 val timing = #timing o rep;
 
+end;
+
 val out = trim_line o cat_lines o out_lines;
 val err = trim_line o cat_lines o err_lines;
 
@@ -49,5 +51,3 @@
 fun check result = if ok result then result else error (err result);
 
 end;
-
-end;