changeset 81920 | 8d5989ab1e42 |
parent 81919 | f4cd3e679096 |
--- a/src/HOL/Import/patches/patch2 Sat Jan 18 22:41:33 2025 +0100 +++ b/src/HOL/Import/patches/patch2 Sat Jan 18 23:19:23 2025 +0100 @@ -5,7 +5,7 @@ needs "lib.ml";; +#load "unix.cma";; -+let poutc = Unix.open_process_out "buffer | gzip -c > proofs.gz";; ++let poutc = open_out "proofs";; +let foutc = open_out "facts.lst";; +let stop_recording () = close_out poutc; close_out foutc;; +