# HG changeset patch
# User wenzelm
# Date 1723633839 -7200
# Node ID 51525e85fcac7a443639aa9ca94fa4daf7641fa3
# Parent  cc4ecaa8e96eb2b9b09f8fc4119dd62e786f52a6
clarified context data;
tuned: more antiquotations;

diff -r cc4ecaa8e96e -r 51525e85fcac src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Tue Aug 13 21:09:51 2024 +0200
+++ b/src/HOL/Tools/record.ML	Wed Aug 14 13:10:39 2024 +0200
@@ -363,6 +363,14 @@
 
 (* theory data *)
 
+type splits = {Pure_all: thm, All: thm, Ex: thm, induct_scheme: thm};
+
+fun eq_splits (arg: splits * splits) =
+  Thm.eq_thm (apply2 #Pure_all arg) andalso
+  Thm.eq_thm (apply2 #All arg) andalso
+  Thm.eq_thm (apply2 #Ex arg) andalso
+  Thm.eq_thm (apply2 #induct_scheme arg);
+
 type data =
  {records: info Symtab.table,
   sel_upd:
@@ -373,7 +381,7 @@
   equalities: thm Symtab.table,
   extinjects: thm list,
   extsplit: thm Symtab.table,  (*maps extension name to split rule*)
-  splits: (thm * thm * thm * thm) Symtab.table,  (*!!, ALL, EX - split-equalities, induct rule*)
+  splits: splits Symtab.table,  (*\<And>/\<forall>/\<exists>-split-equalities, induct rule*)
   extfields: (string * typ) list Symtab.table,  (*maps extension to its fields*)
   fieldext: (string * typ list) Symtab.table};  (*maps field to its extension*)
 
@@ -417,9 +425,7 @@
       (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
       (Thm.merge_thms (extinjects1, extinjects2))
       (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
-      (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
-          Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
-          Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
+      (Symtab.merge eq_splits (splits1, splits2))
       (Symtab.merge (K true) (extfields1, extfields2))
       (Symtab.merge (K true) (fieldext1, fieldext2));
 );
@@ -1324,30 +1330,25 @@
    {name = "record_split",
     lhss = [\<^term>\<open>x::'a::{}\<close>],
     proc = fn _ => fn ctxt => fn ct =>
-      (case Thm.term_of ct of
-        Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
-          if quantifier = \<^const_name>\<open>Pure.all\<close> orelse
-            quantifier = \<^const_name>\<open>All\<close> orelse
-            quantifier = \<^const_name>\<open>Ex\<close>
-          then
-            (case rec_id ~1 T of
-              "" => NONE
-            | _ =>
-                let val split = P (Thm.term_of ct) in
-                  if split <> 0 then
-                    (case get_splits (Proof_Context.theory_of ctxt) (rec_id split T) of
-                      NONE => NONE
-                    | SOME (all_thm, All_thm, Ex_thm, _) =>
-                        SOME
-                          (case quantifier of
-                            \<^const_name>\<open>Pure.all\<close> => all_thm
-                          | \<^const_name>\<open>All\<close> => All_thm RS @{thm eq_reflection}
-                          | \<^const_name>\<open>Ex\<close> => Ex_thm RS @{thm eq_reflection}
-                          | _ => raise Fail "split_simproc"))
-                  else NONE
-                end)
-          else NONE
-      | _ => NONE),
+      let
+        fun quantifier T which =
+          (case rec_id ~1 T of
+            "" => NONE
+          | _ =>
+              let val split = P (Thm.term_of ct) in
+                if split <> 0 then
+                  (case get_splits (Proof_Context.theory_of ctxt) (rec_id split T) of
+                    NONE => NONE
+                  | SOME thms => SOME (which thms))
+                else NONE
+              end)
+      in
+        (case Thm.term_of ct of
+          \<^Const_>\<open>Pure.all T for _\<close> => quantifier T #Pure_all
+        | \<^Const_>\<open>All T for _\<close> => quantifier T #All
+        | \<^Const_>\<open>Ex T for _\<close> => quantifier T #Ex
+        | _ => NONE)
+      end,
     identifier = []};
 
 fun ex_sel_eq_proc ctxt ct =
@@ -1437,8 +1438,7 @@
               if split <> 0 then
                 (case get_splits thy (rec_id split T) of
                   NONE => NONE
-                | SOME (_, _, _, induct_thm) =>
-                    SOME (mk_split_free_tac free induct_thm i))
+                | SOME thms => SOME (mk_split_free_tac free (#induct_scheme thms) i))
               else NONE
             end));
 
@@ -2272,7 +2272,11 @@
       |> add_equalities extension_id equality'
       |> add_extinjects ext_inject
       |> add_extsplit extension_name ext_split
-      |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
+      |> add_splits extension_id
+          {Pure_all = split_meta',
+           All = split_object' RS @{thm eq_reflection},
+           Ex = split_ex' RS @{thm eq_reflection},
+           induct_scheme = induct_scheme'}
       |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
       |> add_fieldext (extension_name, snd extension) names
       |> add_code ext_tyco vs extT ext simps' ext_inject