src/HOL/Import/patches/patch2
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;;
 +