# HG changeset patch
# User wenzelm
# Date 1737235787 -3600
# Node ID deb6cb34a37fe8dc59a926f381bfb480d2533997
# Parent  50cd5037aff77872e73b9e727115e72715b94bae
clarified patches;

diff -r 50cd5037aff7 -r deb6cb34a37f src/HOL/Import/patches/patch1
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/patches/patch1	Sat Jan 18 22:29:47 2025 +0100
@@ -0,0 +1,25 @@
+--- hol-light/statements.ml	1970-01-01 01:00:00.000000000 +0100
++++ hol-light-patched/statements.ml	2025-01-18 11:12:11.185279392 +0100
+@@ -0,0 +1,15 @@
++let name2pairs acc (name, th) =
++  let acc =
++    if is_conj (concl th) then
++      let fold_fun (no, acc) th = (no + 1, (name ^ "_conjunct" ^ (string_of_int no), th) :: acc) in
++      snd (List.fold_left fold_fun (0, acc) (CONJUNCTS th))
++    else acc
++  in (name, th) :: acc
++;;
++let dump_theorems () =
++  let oc = open_out "theorems" in
++  let all_thms = List.fold_left name2pairs [] !theorems in
++  output_value oc (map (fun (a,b) -> (a, dest_thm b)) all_thms);
++  close_out oc
++;;
++dump_theorems ();;
+--- hol-light/stage1.ml	1970-01-01 01:00:00.000000000 +0100
++++ hol-light-patched/stage1.ml	2025-01-18 11:12:11.185279392 +0100
+@@ -0,0 +1,4 @@
++#use "hol.ml";;
++#use "update_database.ml";;
++#use "statements.ml";;
++exit 0;;
diff -r 50cd5037aff7 -r deb6cb34a37f src/HOL/Import/patches/patch2
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/patches/patch2	Sat Jan 18 22:29:47 2025 +0100
@@ -0,0 +1,374 @@
+--- hol-light/fusion.ml	2025-01-18 11:11:28.417955236 +0100
++++ hol-light-patched/fusion.ml	2025-01-18 11:12:11.384276293 +0100
+@@ -9,6 +9,18 @@
+ 
+ needs "lib.ml";;
+ 
++#load "unix.cma";;
++let poutc = Unix.open_process_out "buffer | gzip -c > proofs.gz";;
++let foutc = open_out "facts.lst";;
++let stop_recording () = close_out poutc; close_out foutc;;
++
++let rec outl = function
++  [] -> ()
++| (h :: t) -> try
++    output_string poutc h; List.fold_left
++      (fun () e -> output_char poutc ' '; output_string poutc e) () t
++    with Sys_error _ -> ();;
++
+ module type Hol_kernel =
+   sig
+       type hol_type = private
+@@ -101,7 +113,165 @@
+             | Comb of term * term
+             | Abs of term * term
+ 
+-  type thm = Sequent of (term list * term)
++  type thm = Sequent of (term list * term * int)
++(* PROOFRECORDING BEGIN *)
++let thms = Hashtbl.create 20000;;
++
++let inc = open_in "theorems";;
++let l = ((input_value inc) : ((string * (term list * term)) list));;
++close_in inc;;
++List.iter (fun (n,t) -> Hashtbl.replace thms t (n, 0)) l;;
++print_endline ("Read in: " ^ string_of_int (Hashtbl.length thms));;
++
++module Fm = Map.Make(struct type t = float let compare = compare end);;
++module Tys = Map.Make(struct type t = hol_type let compare = compare end);;
++module Tms = Map.Make(struct type t = term let compare = compare end);;
++module Ps = Map.Make(struct type t = (term list * term) let compare = compare end);;
++
++let ty_no = ref 0;;
++let tys = ref Tys.empty;;
++
++let rec out_type ty =
++  try
++    Tys.find ty !tys
++  with Not_found ->
++    match ty with
++      Tyvar t ->
++        incr ty_no; tys := Tys.add ty !ty_no !tys;
++        output_char poutc 't'; output_string poutc t; output_char poutc '\n';
++        !ty_no
++    | Tyapp (id, tl) ->
++        let tln = map out_type tl in
++        incr ty_no; tys := Tys.add ty !ty_no !tys;
++        output_char poutc 'a'; output_string poutc id; output_char poutc ' ';
++          outl (map string_of_int tln); output_char poutc '\n';
++        !ty_no;;
++
++let tm_no = ref 0;;
++let tms = ref Tms.empty;;
++let tms_prio = ref Fm.empty;;
++let tms_size = ref 0;;
++let tms_maxsize = ref (int_of_string (Sys.getenv "MAXTMS"));;
++let tm_lookup tm =
++  let (ret, oldtime) = Tms.find tm !tms in
++  let newtime = Unix.gettimeofday () in
++  tms := Tms.add tm (ret, newtime) !tms;
++  tms_prio := Fm.add newtime tm (Fm.remove oldtime !tms_prio);
++  ret;;
++
++let tm_delete () =
++  let (time, tm) = Fm.min_binding !tms_prio in
++  tms := Tms.remove tm !tms;
++  tms_prio := Fm.remove time !tms_prio;
++  decr tms_size; ();;
++
++let tm_add tm no =
++  while (!tms_size > !tms_maxsize) do tm_delete (); done;
++  let newtime = Unix.gettimeofday () in
++  tms := Tms.add tm (no, newtime) (!tms);
++  tms_prio := Fm.add newtime tm (!tms_prio);
++  incr tms_size; ();;
++
++let rec out_term tm =
++  try
++    tm_lookup tm
++  with Not_found ->
++    let outc = output_char poutc and out = output_string poutc in
++    match tm with
++      Var (name, ty) ->
++        let ty = out_type ty in
++        incr tm_no; tm_add tm !tm_no;
++        outc 'v'; out name; outc ' '; out (string_of_int ty); outc '\n';
++        !tm_no
++    | Const (name, ty) ->
++        let ty = out_type ty in
++        incr tm_no; tm_add tm !tm_no;
++        outc 'c'; out name; outc ' '; out (string_of_int ty); outc '\n';
++        !tm_no
++    | Comb (f, a) ->
++        let f = out_term f and a = out_term a in
++        incr tm_no; tm_add tm !tm_no;
++        outc 'f'; out (string_of_int f); outc ' '; out (string_of_int a); outc '\n';
++        !tm_no
++    | Abs (x, a) ->
++        let x = out_term x and a = out_term a in
++        incr tm_no; tm_add tm !tm_no;
++        outc 'l'; out (string_of_int x); outc ' '; out (string_of_int a); outc '\n';
++        !tm_no
++;;
++
++let prf_no = ref 0;;
++let outt tag ss tys tms pfs =
++  let tys = map out_type tys and
++      tms = map out_term tms in
++  try
++    output_char poutc tag;
++    outl (ss @ (map string_of_int tys)
++           @ (map string_of_int tms)
++           @ (map string_of_int pfs));
++    output_char poutc '\n'
++  with Sys_error _ -> ()
++;;
++
++let ps = ref Ps.empty;;
++
++let p_lookup p = Ps.find p !ps;;
++let p_add p no = ps := Ps.singleton p no;;
++
++let mk_prff f = incr prf_no; f (); !prf_no;;
++
++let chk_mk_prff f th =
++  try p_lookup th
++  with Not_found ->
++  try
++    let (name, i) = Hashtbl.find thms th in
++    if i > 0 then i else
++    let i = mk_prff f in
++    (ps := Ps.empty;
++    Hashtbl.replace thms th (name, i);
++    (try output_string foutc (name ^ " " ^ string_of_int i ^ "\n"); flush foutc with Sys_error _ -> ());
++    i)
++  with Not_found ->
++    mk_prff (fun () -> f (); p_add th !prf_no);;
++
++
++let mk_prf t l1 l2 l3 l4 _ = mk_prff (fun () -> outt t l1 l2 l3 l4);;
++let chk_mk_prf t l1 l2 l3 l4 th = chk_mk_prff (fun () -> outt t l1 l2 l3 l4) th;;
++let proof_REFL t th = chk_mk_prf 'R' [] [] [t] [] th;;
++let proof_TRANS (p, q) th = chk_mk_prf 'T' [] [] [] [p; q] th;;
++let proof_MK_COMB (p, q) th = chk_mk_prf 'C' [] [] [] [p; q] th;;
++let proof_ABS x p th = chk_mk_prf 'L' [] [] [x] [p] th;;
++let proof_BETA t th = chk_mk_prf 'B' [] [] [t] [] th;;
++let proof_ASSUME t th = chk_mk_prf 'H' [] [] [t] [] th;;
++let proof_EQ_MP p q th = chk_mk_prf 'E' [] [] [] [p; q] th;;
++let proof_DEDUCT_ANTISYM_RULE (p1,t1) (p2,t2) th =
++  chk_mk_prf 'D' [] [] [] [p1; p2] th;;
++let rec explode_subst = function
++  [] -> []
++| ((y,x)::rest) -> x::y::(explode_subst rest);;
++let proof_INST_TYPE s p th = chk_mk_prf 'Q' [] (explode_subst s) [] [p] th;;
++let proof_INST s p th = chk_mk_prf 'S' [] [] (explode_subst s) [p] th;;
++
++let global_ax_counter = ref 0;;
++let new_axiom_name n = incr global_ax_counter; ("ax_" ^ n ^ "_" ^ string_of_int(!global_ax_counter));;
++let proof_new_axiom axname t th = chk_mk_prf 'A' [axname] [] [t] [] th;;
++let proof_new_definition cname t th =
++  chk_mk_prf 'F' [cname] [] [t] [] th;;
++let proof_new_basic_type_definition tyname (absname, repname) (pt,tt) p th =
++  chk_mk_prf 'Y' [tyname; absname; repname] [] [pt; tt] [p] th;;
++let proof_CONJUNCT1 p th = chk_mk_prf '1' [] [] [] [p] th;;
++let proof_CONJUNCT2 p th = chk_mk_prf '2' [] [] [] [p] th;;
++
++let clean_ts_at_saved = ((try Sys.getenv "CLEANTMS" with _ -> "") = "YES");;
++
++let save_proof name p th =
++  Hashtbl.replace thms th (name, p);
++  ps := Ps.empty;
++  if clean_ts_at_saved then (
++    tms := Tms.empty; tms_prio := Fm.empty; tms_size := 0;
++   );
++  (try output_string foutc (name ^ " " ^ string_of_int p ^ "\n"); flush foutc with Sys_error _ -> ());;
++(* PROOFRECORDING END *)
+ 
+ (* ------------------------------------------------------------------------- *)
+ (* List of current type constants with their arities.                        *)
+@@ -485,43 +655,48 @@
+ (* Basic theorem destructors.                                                *)
+ (* ------------------------------------------------------------------------- *)
+ 
+-  let dest_thm (Sequent(asl,c)) = (asl,c)
++  let dest_thm (Sequent(asl,c,_)) = (asl,c)
+ 
+-  let hyp (Sequent(asl,c)) = asl
++  let hyp (Sequent(asl,c,_)) = asl
+ 
+-  let concl (Sequent(asl,c)) = c
++  let concl (Sequent(asl,c,_)) = c
+ 
+ (* ------------------------------------------------------------------------- *)
+ (* Basic equality properties; TRANS is derivable but included for efficiency *)
+ (* ------------------------------------------------------------------------- *)
+ 
+   let REFL tm =
+-    Sequent([],safe_mk_eq tm tm)
++    let eq = safe_mk_eq tm tm in
++    Sequent([],eq,proof_REFL tm ([], eq))
+ 
+-  let TRANS (Sequent(asl1,c1)) (Sequent(asl2,c2)) =
++  let TRANS (Sequent(asl1,c1,p1)) (Sequent(asl2,c2,p2)) =
+     match (c1,c2) with
+       Comb((Comb(Const("=",_),_) as eql),m1),Comb(Comb(Const("=",_),m2),r)
+-        when alphaorder m1 m2 = 0 -> Sequent(term_union asl1 asl2,Comb(eql,r))
++        when alphaorder m1 m2 = 0 ->
++          let (a, g) = (term_union asl1 asl2,Comb(eql,r)) in
++          Sequent (a, g, proof_TRANS (p1, p2) (a, g))
+     | _ -> failwith "TRANS"
+ 
+ (* ------------------------------------------------------------------------- *)
+ (* Congruence properties of equality.                                        *)
+ (* ------------------------------------------------------------------------- *)
+ 
+-  let MK_COMB(Sequent(asl1,c1),Sequent(asl2,c2)) =
++  let MK_COMB(Sequent(asl1,c1,p1),Sequent(asl2,c2,p2)) =
+      match (c1,c2) with
+        Comb(Comb(Const("=",_),l1),r1),Comb(Comb(Const("=",_),l2),r2) ->
+         (match type_of r1 with
+            Tyapp("fun",[ty;_]) when compare ty (type_of r2) = 0
+-             -> Sequent(term_union asl1 asl2,
+-                        safe_mk_eq (Comb(l1,l2)) (Comb(r1,r2)))
++             -> let (a, g) = (term_union asl1 asl2,
++                        safe_mk_eq (Comb(l1,l2)) (Comb(r1,r2))) in
++                Sequent (a, g, proof_MK_COMB (p1, p2) (a,g))
+          | _ -> failwith "MK_COMB: types do not agree")
+      | _ -> failwith "MK_COMB: not both equations"
+ 
+-  let ABS v (Sequent(asl,c)) =
++  let ABS v (Sequent(asl,c,p)) =
+     match (v,c) with
+       Var(_,_),Comb(Comb(Const("=",_),l),r) when not(exists (vfree_in v) asl)
+-         -> Sequent(asl,safe_mk_eq (Abs(v,l)) (Abs(v,r)))
++         -> let eq = safe_mk_eq (Abs(v,l)) (Abs(v,r)) in
++            Sequent (asl,eq,proof_ABS v p (asl,eq))
+     | _ -> failwith "ABS";;
+ 
+ (* ------------------------------------------------------------------------- *)
+@@ -531,7 +706,8 @@
+   let BETA tm =
+     match tm with
+       Comb(Abs(v,bod),arg) when compare arg v = 0
+-        -> Sequent([],safe_mk_eq tm bod)
++        -> let eq = safe_mk_eq tm bod in
++           Sequent([],eq,proof_BETA tm ([], eq))
+     | _ -> failwith "BETA: not a trivial beta-redex"
+ 
+ (* ------------------------------------------------------------------------- *)
+@@ -539,30 +715,35 @@
+ (* ------------------------------------------------------------------------- *)
+ 
+   let ASSUME tm =
+-    if compare (type_of tm) bool_ty = 0 then Sequent([tm],tm)
++    if compare (type_of tm) bool_ty = 0 then
++      Sequent([tm],tm,proof_ASSUME tm ([tm], tm))
+     else failwith "ASSUME: not a proposition"
+ 
+-  let EQ_MP (Sequent(asl1,eq)) (Sequent(asl2,c)) =
++  let EQ_MP (Sequent(asl1,eq,p1)) (Sequent(asl2,c,p2)) =
+     match eq with
+       Comb(Comb(Const("=",_),l),r) when alphaorder l c = 0
+-        -> Sequent(term_union asl1 asl2,r)
++        -> let t = term_union asl1 asl2 in
++           Sequent(t,r,proof_EQ_MP p1 p2 (t,r))
+     | _ -> failwith "EQ_MP"
+ 
+-  let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1)) (Sequent(asl2,c2)) =
++  let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1,p1)) (Sequent(asl2,c2,p2)) =
+     let asl1' = term_remove c2 asl1 and asl2' = term_remove c1 asl2 in
+-    Sequent(term_union asl1' asl2',safe_mk_eq c1 c2)
++    let (a,g) = (term_union asl1' asl2',safe_mk_eq c1 c2) in
++    Sequent (a, g, proof_DEDUCT_ANTISYM_RULE (p1,c1) (p2,c2) (a, g))
+ 
+ (* ------------------------------------------------------------------------- *)
+ (* Type and term instantiation.                                              *)
+ (* ------------------------------------------------------------------------- *)
+ 
+-  let INST_TYPE theta (Sequent(asl,c)) =
++  let INST_TYPE theta (Sequent(asl,c,p)) =
+     let inst_fn = inst theta in
+-    Sequent(term_image inst_fn asl,inst_fn c)
++    let (a, g) = (term_image inst_fn asl,inst_fn c) in
++    Sequent(a,g, proof_INST_TYPE theta p (a,g))
+ 
+-  let INST theta (Sequent(asl,c)) =
++  let INST theta (Sequent(asl,c,p)) =
+     let inst_fun = vsubst theta in
+-    Sequent(term_image inst_fun asl,inst_fun c)
++    let (a, g) = (term_image inst_fun asl,inst_fun c) in
++    Sequent(a, g, proof_INST theta p (a,g))
+ 
+ (* ------------------------------------------------------------------------- *)
+ (* Handling of axioms.                                                       *)
+@@ -574,8 +755,11 @@
+ 
+   let new_axiom tm =
+     if compare (type_of tm) bool_ty = 0 then
+-      let th = Sequent([],tm) in
+-       (the_axioms := th::(!the_axioms); th)
++      let axname = new_axiom_name "" in
++      let p = proof_new_axiom axname tm ([], tm) in
++      let th = Sequent([],tm,p) in
++       (the_axioms := th::(!the_axioms);
++        save_proof axname p ([], tm); th)
+     else failwith "new_axiom: Not a proposition"
+ 
+ (* ------------------------------------------------------------------------- *)
+@@ -595,7 +779,10 @@
+         else if not (subset (type_vars_in_term r) (tyvars ty))
+         then failwith "new_definition: Type variables not reflected in constant"
+         else let c = new_constant(cname,ty); Const(cname,ty) in
+-             let dth = Sequent([],safe_mk_eq c r) in
++             let concl = safe_mk_eq c r in
++             let p = proof_new_definition cname r ([], concl) in
++             let dth = Sequent([],concl, p) in
++             save_proof ("DEF_"^cname) p ([], concl);
+              the_definitions := dth::(!the_definitions); dth
+     | Comb(Comb(Const("=",_),Const(cname,ty)),r) ->
+       failwith ("new_basic_definition: '" ^ cname ^ "' is already defined")
+@@ -614,7 +801,7 @@
+ (* Where "abs" and "rep" are new constants with the nominated names.         *)
+ (* ------------------------------------------------------------------------- *)
+ 
+-  let new_basic_type_definition tyname (absname,repname) (Sequent(asl,c)) =
++  let new_basic_type_definition tyname (absname,repname) (Sequent(asl,c,p)) =
+     if exists (can get_const_type) [absname; repname] then
+       failwith "new_basic_type_definition: Constant(s) already in use" else
+     if not (asl = []) then
+@@ -634,9 +821,19 @@
+     let abs = (new_constant(absname,absty); Const(absname,absty))
+     and rep = (new_constant(repname,repty); Const(repname,repty)) in
+     let a = Var("a",aty) and r = Var("r",rty) in
+-    Sequent([],safe_mk_eq (Comb(abs,mk_comb(rep,a))) a),
+-    Sequent([],safe_mk_eq (Comb(P,r))
+-                          (safe_mk_eq (mk_comb(rep,mk_comb(abs,r))) r))
++    let ax1 = safe_mk_eq (Comb(abs,mk_comb(rep,a))) a
++    and ax2 = safe_mk_eq (Comb(P,r)) (safe_mk_eq (mk_comb(rep,mk_comb(abs,r))) r) in
++    let mk_binary s =
++      let c = mk_const(s,[]) in
++      fun (l,r) -> try mk_comb(mk_comb(c,l),r)
++                   with Failure _ -> failwith "tydef_mk_binary"
++    in
++    let axc = mk_binary "/\\" (ax1, ax2) in
++    let tp = proof_new_basic_type_definition tyname (absname, repname) (P,x) p ([], axc) in
++    let p1 = proof_CONJUNCT1 tp ([], ax1) in
++    let p2 = proof_CONJUNCT2 tp ([], ax2) in
++    save_proof ("TYDEF_" ^ tyname) tp ([], axc);
++    (Sequent([],ax1,p1), Sequent([],ax2,p2));;
+ 
+ end;;
+ 
+--- hol-light/stage1.ml	2025-01-18 11:12:11.373276465 +0100
++++ hol-light-patched/stage1.ml	1970-01-01 01:00:00.000000000 +0100
+@@ -1,4 +0,0 @@
+-#use "hol.ml";;
+-#use "update_database.ml";;
+-#use "statements.ml";;
+-exit 0;;
+--- hol-light/stage2.ml	1970-01-01 01:00:00.000000000 +0100
++++ hol-light-patched/stage2.ml	2025-01-18 11:12:11.384276293 +0100
+@@ -0,0 +1,3 @@
++#use "hol.ml";;
++stop_recording ();;
++exit 0;;
diff -r 50cd5037aff7 -r deb6cb34a37f src/HOL/Import/patches/stage1.patch
--- a/src/HOL/Import/patches/stage1.patch	Sat Jan 18 22:25:47 2025 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
---- hol-light/statements.ml	1970-01-01 01:00:00.000000000 +0100
-+++ hol-light-patched/statements.ml	2025-01-18 11:12:11.185279392 +0100
-@@ -0,0 +1,15 @@
-+let name2pairs acc (name, th) =
-+  let acc =
-+    if is_conj (concl th) then
-+      let fold_fun (no, acc) th = (no + 1, (name ^ "_conjunct" ^ (string_of_int no), th) :: acc) in
-+      snd (List.fold_left fold_fun (0, acc) (CONJUNCTS th))
-+    else acc
-+  in (name, th) :: acc
-+;;
-+let dump_theorems () =
-+  let oc = open_out "theorems" in
-+  let all_thms = List.fold_left name2pairs [] !theorems in
-+  output_value oc (map (fun (a,b) -> (a, dest_thm b)) all_thms);
-+  close_out oc
-+;;
-+dump_theorems ();;
---- hol-light/stage1.ml	1970-01-01 01:00:00.000000000 +0100
-+++ hol-light-patched/stage1.ml	2025-01-18 11:12:11.185279392 +0100
-@@ -0,0 +1,4 @@
-+#use "hol.ml";;
-+#use "update_database.ml";;
-+#use "statements.ml";;
-+exit 0;;
diff -r 50cd5037aff7 -r deb6cb34a37f src/HOL/Import/patches/stage2.patch
--- a/src/HOL/Import/patches/stage2.patch	Sat Jan 18 22:25:47 2025 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,374 +0,0 @@
---- hol-light/fusion.ml	2025-01-18 11:11:28.417955236 +0100
-+++ hol-light-patched/fusion.ml	2025-01-18 11:12:11.384276293 +0100
-@@ -9,6 +9,18 @@
- 
- needs "lib.ml";;
- 
-+#load "unix.cma";;
-+let poutc = Unix.open_process_out "buffer | gzip -c > proofs.gz";;
-+let foutc = open_out "facts.lst";;
-+let stop_recording () = close_out poutc; close_out foutc;;
-+
-+let rec outl = function
-+  [] -> ()
-+| (h :: t) -> try
-+    output_string poutc h; List.fold_left
-+      (fun () e -> output_char poutc ' '; output_string poutc e) () t
-+    with Sys_error _ -> ();;
-+
- module type Hol_kernel =
-   sig
-       type hol_type = private
-@@ -101,7 +113,165 @@
-             | Comb of term * term
-             | Abs of term * term
- 
--  type thm = Sequent of (term list * term)
-+  type thm = Sequent of (term list * term * int)
-+(* PROOFRECORDING BEGIN *)
-+let thms = Hashtbl.create 20000;;
-+
-+let inc = open_in "theorems";;
-+let l = ((input_value inc) : ((string * (term list * term)) list));;
-+close_in inc;;
-+List.iter (fun (n,t) -> Hashtbl.replace thms t (n, 0)) l;;
-+print_endline ("Read in: " ^ string_of_int (Hashtbl.length thms));;
-+
-+module Fm = Map.Make(struct type t = float let compare = compare end);;
-+module Tys = Map.Make(struct type t = hol_type let compare = compare end);;
-+module Tms = Map.Make(struct type t = term let compare = compare end);;
-+module Ps = Map.Make(struct type t = (term list * term) let compare = compare end);;
-+
-+let ty_no = ref 0;;
-+let tys = ref Tys.empty;;
-+
-+let rec out_type ty =
-+  try
-+    Tys.find ty !tys
-+  with Not_found ->
-+    match ty with
-+      Tyvar t ->
-+        incr ty_no; tys := Tys.add ty !ty_no !tys;
-+        output_char poutc 't'; output_string poutc t; output_char poutc '\n';
-+        !ty_no
-+    | Tyapp (id, tl) ->
-+        let tln = map out_type tl in
-+        incr ty_no; tys := Tys.add ty !ty_no !tys;
-+        output_char poutc 'a'; output_string poutc id; output_char poutc ' ';
-+          outl (map string_of_int tln); output_char poutc '\n';
-+        !ty_no;;
-+
-+let tm_no = ref 0;;
-+let tms = ref Tms.empty;;
-+let tms_prio = ref Fm.empty;;
-+let tms_size = ref 0;;
-+let tms_maxsize = ref (int_of_string (Sys.getenv "MAXTMS"));;
-+let tm_lookup tm =
-+  let (ret, oldtime) = Tms.find tm !tms in
-+  let newtime = Unix.gettimeofday () in
-+  tms := Tms.add tm (ret, newtime) !tms;
-+  tms_prio := Fm.add newtime tm (Fm.remove oldtime !tms_prio);
-+  ret;;
-+
-+let tm_delete () =
-+  let (time, tm) = Fm.min_binding !tms_prio in
-+  tms := Tms.remove tm !tms;
-+  tms_prio := Fm.remove time !tms_prio;
-+  decr tms_size; ();;
-+
-+let tm_add tm no =
-+  while (!tms_size > !tms_maxsize) do tm_delete (); done;
-+  let newtime = Unix.gettimeofday () in
-+  tms := Tms.add tm (no, newtime) (!tms);
-+  tms_prio := Fm.add newtime tm (!tms_prio);
-+  incr tms_size; ();;
-+
-+let rec out_term tm =
-+  try
-+    tm_lookup tm
-+  with Not_found ->
-+    let outc = output_char poutc and out = output_string poutc in
-+    match tm with
-+      Var (name, ty) ->
-+        let ty = out_type ty in
-+        incr tm_no; tm_add tm !tm_no;
-+        outc 'v'; out name; outc ' '; out (string_of_int ty); outc '\n';
-+        !tm_no
-+    | Const (name, ty) ->
-+        let ty = out_type ty in
-+        incr tm_no; tm_add tm !tm_no;
-+        outc 'c'; out name; outc ' '; out (string_of_int ty); outc '\n';
-+        !tm_no
-+    | Comb (f, a) ->
-+        let f = out_term f and a = out_term a in
-+        incr tm_no; tm_add tm !tm_no;
-+        outc 'f'; out (string_of_int f); outc ' '; out (string_of_int a); outc '\n';
-+        !tm_no
-+    | Abs (x, a) ->
-+        let x = out_term x and a = out_term a in
-+        incr tm_no; tm_add tm !tm_no;
-+        outc 'l'; out (string_of_int x); outc ' '; out (string_of_int a); outc '\n';
-+        !tm_no
-+;;
-+
-+let prf_no = ref 0;;
-+let outt tag ss tys tms pfs =
-+  let tys = map out_type tys and
-+      tms = map out_term tms in
-+  try
-+    output_char poutc tag;
-+    outl (ss @ (map string_of_int tys)
-+           @ (map string_of_int tms)
-+           @ (map string_of_int pfs));
-+    output_char poutc '\n'
-+  with Sys_error _ -> ()
-+;;
-+
-+let ps = ref Ps.empty;;
-+
-+let p_lookup p = Ps.find p !ps;;
-+let p_add p no = ps := Ps.singleton p no;;
-+
-+let mk_prff f = incr prf_no; f (); !prf_no;;
-+
-+let chk_mk_prff f th =
-+  try p_lookup th
-+  with Not_found ->
-+  try
-+    let (name, i) = Hashtbl.find thms th in
-+    if i > 0 then i else
-+    let i = mk_prff f in
-+    (ps := Ps.empty;
-+    Hashtbl.replace thms th (name, i);
-+    (try output_string foutc (name ^ " " ^ string_of_int i ^ "\n"); flush foutc with Sys_error _ -> ());
-+    i)
-+  with Not_found ->
-+    mk_prff (fun () -> f (); p_add th !prf_no);;
-+
-+
-+let mk_prf t l1 l2 l3 l4 _ = mk_prff (fun () -> outt t l1 l2 l3 l4);;
-+let chk_mk_prf t l1 l2 l3 l4 th = chk_mk_prff (fun () -> outt t l1 l2 l3 l4) th;;
-+let proof_REFL t th = chk_mk_prf 'R' [] [] [t] [] th;;
-+let proof_TRANS (p, q) th = chk_mk_prf 'T' [] [] [] [p; q] th;;
-+let proof_MK_COMB (p, q) th = chk_mk_prf 'C' [] [] [] [p; q] th;;
-+let proof_ABS x p th = chk_mk_prf 'L' [] [] [x] [p] th;;
-+let proof_BETA t th = chk_mk_prf 'B' [] [] [t] [] th;;
-+let proof_ASSUME t th = chk_mk_prf 'H' [] [] [t] [] th;;
-+let proof_EQ_MP p q th = chk_mk_prf 'E' [] [] [] [p; q] th;;
-+let proof_DEDUCT_ANTISYM_RULE (p1,t1) (p2,t2) th =
-+  chk_mk_prf 'D' [] [] [] [p1; p2] th;;
-+let rec explode_subst = function
-+  [] -> []
-+| ((y,x)::rest) -> x::y::(explode_subst rest);;
-+let proof_INST_TYPE s p th = chk_mk_prf 'Q' [] (explode_subst s) [] [p] th;;
-+let proof_INST s p th = chk_mk_prf 'S' [] [] (explode_subst s) [p] th;;
-+
-+let global_ax_counter = ref 0;;
-+let new_axiom_name n = incr global_ax_counter; ("ax_" ^ n ^ "_" ^ string_of_int(!global_ax_counter));;
-+let proof_new_axiom axname t th = chk_mk_prf 'A' [axname] [] [t] [] th;;
-+let proof_new_definition cname t th =
-+  chk_mk_prf 'F' [cname] [] [t] [] th;;
-+let proof_new_basic_type_definition tyname (absname, repname) (pt,tt) p th =
-+  chk_mk_prf 'Y' [tyname; absname; repname] [] [pt; tt] [p] th;;
-+let proof_CONJUNCT1 p th = chk_mk_prf '1' [] [] [] [p] th;;
-+let proof_CONJUNCT2 p th = chk_mk_prf '2' [] [] [] [p] th;;
-+
-+let clean_ts_at_saved = ((try Sys.getenv "CLEANTMS" with _ -> "") = "YES");;
-+
-+let save_proof name p th =
-+  Hashtbl.replace thms th (name, p);
-+  ps := Ps.empty;
-+  if clean_ts_at_saved then (
-+    tms := Tms.empty; tms_prio := Fm.empty; tms_size := 0;
-+   );
-+  (try output_string foutc (name ^ " " ^ string_of_int p ^ "\n"); flush foutc with Sys_error _ -> ());;
-+(* PROOFRECORDING END *)
- 
- (* ------------------------------------------------------------------------- *)
- (* List of current type constants with their arities.                        *)
-@@ -485,43 +655,48 @@
- (* Basic theorem destructors.                                                *)
- (* ------------------------------------------------------------------------- *)
- 
--  let dest_thm (Sequent(asl,c)) = (asl,c)
-+  let dest_thm (Sequent(asl,c,_)) = (asl,c)
- 
--  let hyp (Sequent(asl,c)) = asl
-+  let hyp (Sequent(asl,c,_)) = asl
- 
--  let concl (Sequent(asl,c)) = c
-+  let concl (Sequent(asl,c,_)) = c
- 
- (* ------------------------------------------------------------------------- *)
- (* Basic equality properties; TRANS is derivable but included for efficiency *)
- (* ------------------------------------------------------------------------- *)
- 
-   let REFL tm =
--    Sequent([],safe_mk_eq tm tm)
-+    let eq = safe_mk_eq tm tm in
-+    Sequent([],eq,proof_REFL tm ([], eq))
- 
--  let TRANS (Sequent(asl1,c1)) (Sequent(asl2,c2)) =
-+  let TRANS (Sequent(asl1,c1,p1)) (Sequent(asl2,c2,p2)) =
-     match (c1,c2) with
-       Comb((Comb(Const("=",_),_) as eql),m1),Comb(Comb(Const("=",_),m2),r)
--        when alphaorder m1 m2 = 0 -> Sequent(term_union asl1 asl2,Comb(eql,r))
-+        when alphaorder m1 m2 = 0 ->
-+          let (a, g) = (term_union asl1 asl2,Comb(eql,r)) in
-+          Sequent (a, g, proof_TRANS (p1, p2) (a, g))
-     | _ -> failwith "TRANS"
- 
- (* ------------------------------------------------------------------------- *)
- (* Congruence properties of equality.                                        *)
- (* ------------------------------------------------------------------------- *)
- 
--  let MK_COMB(Sequent(asl1,c1),Sequent(asl2,c2)) =
-+  let MK_COMB(Sequent(asl1,c1,p1),Sequent(asl2,c2,p2)) =
-      match (c1,c2) with
-        Comb(Comb(Const("=",_),l1),r1),Comb(Comb(Const("=",_),l2),r2) ->
-         (match type_of r1 with
-            Tyapp("fun",[ty;_]) when compare ty (type_of r2) = 0
--             -> Sequent(term_union asl1 asl2,
--                        safe_mk_eq (Comb(l1,l2)) (Comb(r1,r2)))
-+             -> let (a, g) = (term_union asl1 asl2,
-+                        safe_mk_eq (Comb(l1,l2)) (Comb(r1,r2))) in
-+                Sequent (a, g, proof_MK_COMB (p1, p2) (a,g))
-          | _ -> failwith "MK_COMB: types do not agree")
-      | _ -> failwith "MK_COMB: not both equations"
- 
--  let ABS v (Sequent(asl,c)) =
-+  let ABS v (Sequent(asl,c,p)) =
-     match (v,c) with
-       Var(_,_),Comb(Comb(Const("=",_),l),r) when not(exists (vfree_in v) asl)
--         -> Sequent(asl,safe_mk_eq (Abs(v,l)) (Abs(v,r)))
-+         -> let eq = safe_mk_eq (Abs(v,l)) (Abs(v,r)) in
-+            Sequent (asl,eq,proof_ABS v p (asl,eq))
-     | _ -> failwith "ABS";;
- 
- (* ------------------------------------------------------------------------- *)
-@@ -531,7 +706,8 @@
-   let BETA tm =
-     match tm with
-       Comb(Abs(v,bod),arg) when compare arg v = 0
--        -> Sequent([],safe_mk_eq tm bod)
-+        -> let eq = safe_mk_eq tm bod in
-+           Sequent([],eq,proof_BETA tm ([], eq))
-     | _ -> failwith "BETA: not a trivial beta-redex"
- 
- (* ------------------------------------------------------------------------- *)
-@@ -539,30 +715,35 @@
- (* ------------------------------------------------------------------------- *)
- 
-   let ASSUME tm =
--    if compare (type_of tm) bool_ty = 0 then Sequent([tm],tm)
-+    if compare (type_of tm) bool_ty = 0 then
-+      Sequent([tm],tm,proof_ASSUME tm ([tm], tm))
-     else failwith "ASSUME: not a proposition"
- 
--  let EQ_MP (Sequent(asl1,eq)) (Sequent(asl2,c)) =
-+  let EQ_MP (Sequent(asl1,eq,p1)) (Sequent(asl2,c,p2)) =
-     match eq with
-       Comb(Comb(Const("=",_),l),r) when alphaorder l c = 0
--        -> Sequent(term_union asl1 asl2,r)
-+        -> let t = term_union asl1 asl2 in
-+           Sequent(t,r,proof_EQ_MP p1 p2 (t,r))
-     | _ -> failwith "EQ_MP"
- 
--  let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1)) (Sequent(asl2,c2)) =
-+  let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1,p1)) (Sequent(asl2,c2,p2)) =
-     let asl1' = term_remove c2 asl1 and asl2' = term_remove c1 asl2 in
--    Sequent(term_union asl1' asl2',safe_mk_eq c1 c2)
-+    let (a,g) = (term_union asl1' asl2',safe_mk_eq c1 c2) in
-+    Sequent (a, g, proof_DEDUCT_ANTISYM_RULE (p1,c1) (p2,c2) (a, g))
- 
- (* ------------------------------------------------------------------------- *)
- (* Type and term instantiation.                                              *)
- (* ------------------------------------------------------------------------- *)
- 
--  let INST_TYPE theta (Sequent(asl,c)) =
-+  let INST_TYPE theta (Sequent(asl,c,p)) =
-     let inst_fn = inst theta in
--    Sequent(term_image inst_fn asl,inst_fn c)
-+    let (a, g) = (term_image inst_fn asl,inst_fn c) in
-+    Sequent(a,g, proof_INST_TYPE theta p (a,g))
- 
--  let INST theta (Sequent(asl,c)) =
-+  let INST theta (Sequent(asl,c,p)) =
-     let inst_fun = vsubst theta in
--    Sequent(term_image inst_fun asl,inst_fun c)
-+    let (a, g) = (term_image inst_fun asl,inst_fun c) in
-+    Sequent(a, g, proof_INST theta p (a,g))
- 
- (* ------------------------------------------------------------------------- *)
- (* Handling of axioms.                                                       *)
-@@ -574,8 +755,11 @@
- 
-   let new_axiom tm =
-     if compare (type_of tm) bool_ty = 0 then
--      let th = Sequent([],tm) in
--       (the_axioms := th::(!the_axioms); th)
-+      let axname = new_axiom_name "" in
-+      let p = proof_new_axiom axname tm ([], tm) in
-+      let th = Sequent([],tm,p) in
-+       (the_axioms := th::(!the_axioms);
-+        save_proof axname p ([], tm); th)
-     else failwith "new_axiom: Not a proposition"
- 
- (* ------------------------------------------------------------------------- *)
-@@ -595,7 +779,10 @@
-         else if not (subset (type_vars_in_term r) (tyvars ty))
-         then failwith "new_definition: Type variables not reflected in constant"
-         else let c = new_constant(cname,ty); Const(cname,ty) in
--             let dth = Sequent([],safe_mk_eq c r) in
-+             let concl = safe_mk_eq c r in
-+             let p = proof_new_definition cname r ([], concl) in
-+             let dth = Sequent([],concl, p) in
-+             save_proof ("DEF_"^cname) p ([], concl);
-              the_definitions := dth::(!the_definitions); dth
-     | Comb(Comb(Const("=",_),Const(cname,ty)),r) ->
-       failwith ("new_basic_definition: '" ^ cname ^ "' is already defined")
-@@ -614,7 +801,7 @@
- (* Where "abs" and "rep" are new constants with the nominated names.         *)
- (* ------------------------------------------------------------------------- *)
- 
--  let new_basic_type_definition tyname (absname,repname) (Sequent(asl,c)) =
-+  let new_basic_type_definition tyname (absname,repname) (Sequent(asl,c,p)) =
-     if exists (can get_const_type) [absname; repname] then
-       failwith "new_basic_type_definition: Constant(s) already in use" else
-     if not (asl = []) then
-@@ -634,9 +821,19 @@
-     let abs = (new_constant(absname,absty); Const(absname,absty))
-     and rep = (new_constant(repname,repty); Const(repname,repty)) in
-     let a = Var("a",aty) and r = Var("r",rty) in
--    Sequent([],safe_mk_eq (Comb(abs,mk_comb(rep,a))) a),
--    Sequent([],safe_mk_eq (Comb(P,r))
--                          (safe_mk_eq (mk_comb(rep,mk_comb(abs,r))) r))
-+    let ax1 = safe_mk_eq (Comb(abs,mk_comb(rep,a))) a
-+    and ax2 = safe_mk_eq (Comb(P,r)) (safe_mk_eq (mk_comb(rep,mk_comb(abs,r))) r) in
-+    let mk_binary s =
-+      let c = mk_const(s,[]) in
-+      fun (l,r) -> try mk_comb(mk_comb(c,l),r)
-+                   with Failure _ -> failwith "tydef_mk_binary"
-+    in
-+    let axc = mk_binary "/\\" (ax1, ax2) in
-+    let tp = proof_new_basic_type_definition tyname (absname, repname) (P,x) p ([], axc) in
-+    let p1 = proof_CONJUNCT1 tp ([], ax1) in
-+    let p2 = proof_CONJUNCT2 tp ([], ax2) in
-+    save_proof ("TYDEF_" ^ tyname) tp ([], axc);
-+    (Sequent([],ax1,p1), Sequent([],ax2,p2));;
- 
- end;;
- 
---- hol-light/stage1.ml	2025-01-18 11:12:11.373276465 +0100
-+++ hol-light-patched/stage1.ml	1970-01-01 01:00:00.000000000 +0100
-@@ -1,4 +0,0 @@
--#use "hol.ml";;
--#use "update_database.ml";;
--#use "statements.ml";;
--exit 0;;
---- hol-light/stage2.ml	1970-01-01 01:00:00.000000000 +0100
-+++ hol-light-patched/stage2.ml	2025-01-18 11:12:11.384276293 +0100
-@@ -0,0 +1,3 @@
-+#use "hol.ml";;
-+stop_recording ();;
-+exit 0;;
diff -r 50cd5037aff7 -r deb6cb34a37f src/Pure/Admin/component_hol_light.scala
--- a/src/Pure/Admin/component_hol_light.scala	Sat Jan 18 22:25:47 2025 +0100
+++ b/src/Pure/Admin/component_hol_light.scala	Sat Jan 18 22:29:47 2025 +0100
@@ -15,8 +15,6 @@
   val default_hol_light_rev = "Release-3.0.0"
 
   val hol_import_dir: Path = Path.explode("~~/src/HOL/Import")
-  def patch1: Path = hol_import_dir + Path.explode("patches/stage1.patch")
-  def patch2: Path = hol_import_dir + Path.explode("patches/stage2.patch")
 
   def build_hol_light_import(
     only_offline: Boolean = false,
@@ -66,15 +64,15 @@
 This is an export of primitive proofs from HOL Light """ + hol_light_rev + """.
 
 The original repository """ + hol_light_url + """
-has been patched in 2 stages. The overall export process works like this:
+has been patched in 2 phases. The overall export process works like this:
 
   cd hol-light
   make
 
-  patch -p1 < """ + patch1 + """
+  patch -p1 < "$HOL_LIGHT_IMPORT/patches/patch1"
   ./ocaml-hol -I +compiler-libs stage1.ml
 
-  patch -p1 < """ + patch2 + """
+  patch -p1 < "$HOL_LIGHT_IMPORT/patches/patch2"
   export MAXTMS=10000
   ./ocaml-hol -I +compiler-libs stage2.ml
 
@@ -116,20 +114,33 @@
       File.set_executable(platform_dir + offline_exe)
 
 
-      /* export */
+      if (!only_offline) {
+        /* clone repository */
 
-      if (!only_offline) {
         val hol_light_dir = tmp_dir + Path.basic("hol-light")
         Isabelle_System.git_clone(hol_light_url, hol_light_dir, checkout = hol_light_rev,
           progress = progress)
 
+
+        /* patches */
+
+        Isabelle_System.make_directory(component_dir.path + Path.basic("patches"))
+
+        def patch(n: Int, source: Boolean = false): Path =
+          (if (source) hol_import_dir else component_dir.path) + Path.explode("patches/patch" + n)
+
+        for (n <- List(1, 2)) Isabelle_System.copy_file(patch(n, source = true), patch(n))
+
+
+        /* export stages */
+
         def run(n: Int, lines: String*): Unit = {
           val title = "stage " + n
           if (n > 0) progress.echo("Running " + title + " ...")
 
           val start = Time.now()
           progress.bash(cat_lines("set -e" :: opam_env :: lines.toList),
-            cwd = hol_light_dir, echo = progress.verbose).check
+            cwd = hol_light_dir, echo = progress.verbose).check.timing
           val elapsed = Time.now() - start
 
           if (n > 0) {
@@ -139,10 +150,10 @@
 
         run(0, "make")
         run(1,
-          "patch -p1 < " + File.bash_path(patch1),
+          "patch -p1 < " + File.bash_path(patch(1)),
           "./ocaml-hol -I +compiler-libs stage1.ml")
         run(2,
-          "patch -p1 < " + File.bash_path(patch2),
+          "patch -p1 < " + File.bash_path(patch(2)),
           "export MAXTMS=10000",
           "./ocaml-hol -I +compiler-libs stage2.ml")
         run(3,