src/HOL/Import/patches/patch1

 --- 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
-+;;
+@@ -0,0 +1,6 @@
 +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);
++  output_value oc (map (fun (a,b) -> (a, dest_thm b)) !theorems);
 +  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