# HG changeset patch
# User wenzelm
# Date 1737371496 -3600
# Node ID 3c888cd24351d812ab9c8cc1afec9a0a09ecddac
# Parent  8c8726e82b71fde74e86664154b3ec19b598f0fa
discontinue special treatment of HOL Light CONJUNCTS: this is better done in Isabelle;

diff -r 8c8726e82b71 -r 3c888cd24351 src/HOL/Import/offline/maps.lst
--- a/src/HOL/Import/offline/maps.lst	Mon Jan 20 11:38:47 2025 +0100
+++ b/src/HOL/Import/offline/maps.lst	Mon Jan 20 12:11:36 2025 +0100
@@ -82,8 +82,6 @@
 DEF_APPEND    -
 APPEND        APPEND
 DEF_REVERSE   -
-REVERSE_conjunct0 REVERSE(0)
-REVERSE_conjunct1 REVERSE(1)
 DEF_LENGTH    -
 LENGTH        LENGTH
 DEF_MAP       -
@@ -91,35 +89,15 @@
 DEF_LAST      -
 LAST          LAST
 DEF_BUTLAST   -
-BUTLAST_conjunct0 BUTLAST(0)
-BUTLAST_conjunct1 BUTLAST(1)
 DEF_REPLICATE -
-REPLICATE_conjunct0 REPLICATE(0)
-REPLICATE_conjunct1 REPLICATE(1)
 DEF_NULL      -
-NULL_conjunct0 NULL(0)
-NULL_conjunct1 NULL(1)
 DEF_ALL       -
-ALL_conjunct0 ALL(0)
-ALL_conjunct1 ALL(1)
 DEF_EX        -
-EX_conjunct0  EX(0)
-EX_conjunct1  EX(1)
 DEF_ITLIST    -
-ITLIST_conjunct0 ITLIST(0)
-ITLIST_conjunct1 ITLIST(1)
 DEF_ALL2      -
-ALL2_DEF_conjunct0 ALL2_DEF(0)
-ALL2_DEF_conjunct1 ALL2_DEF(1)
 DEF_FILTER    -
-FILTER_conjunct0 FILTER(0)
-FILTER_conjunct1 FILTER(1)
 DEF_ZIP       -
-ZIP_DEF_conjunct0 -
-ZIP_DEF_conjunct1 -
 ZIP_DEF       -
-ZIP_conjunct0 ZIP(0)
-ZIP_conjunct1 ZIP(1)
 TYDEF_real -
 DEF_real_of_num -
 real_of_num -
@@ -165,8 +143,6 @@
 DEF_real_abs -
 real_abs real_abs
 DEF_real_pow -
-REAL_POLY_CLAUSES_conjunct9 REAL_POLY_CLAUSES_conjunct9
-REAL_POLY_CLAUSES_conjunct8 REAL_POLY_CLAUSES_conjunct8
 DEF_real_div -
 real_div real_div
 DEF_real_max -
diff -r 8c8726e82b71 -r 3c888cd24351 src/HOL/Import/patches/patch1
--- a/src/HOL/Import/patches/patch1	Mon Jan 20 11:38:47 2025 +0100
+++ b/src/HOL/Import/patches/patch1	Mon Jan 20 12:11:36 2025 +0100
@@ -1,18 +1,9 @@
 --- 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 ();;