# HG changeset patch
# User wenzelm
# Date 1704047077 -3600
# Node ID e1895596e1b9bb791a15e90f83fde662dfd83c00
# Parent  d9cf62ea273d8544f642dbf7ee972a6d3f69b77b
minor performance tuning: proper Same.operation;
clarified modules;

diff -r d9cf62ea273d -r e1895596e1b9 src/HOL/Tools/SMT/z3_proof.ML
--- a/src/HOL/Tools/SMT/z3_proof.ML	Sun Dec 31 18:49:00 2023 +0100
+++ b/src/HOL/Tools/SMT/z3_proof.ML	Sun Dec 31 19:24:37 2023 +0100
@@ -210,7 +210,7 @@
 
 fun substTs_same subst =
   let val applyT = Same.function (AList.lookup (op =) subst)
-  in Term_Subst.map_atypsT_same applyT end
+  in Term.map_atyps_same applyT end
 
 fun subst_types ctxt env bounds t =
   let
@@ -226,7 +226,7 @@
     val patTs = map snd (Term.strip_qnt_vars \<^const_name>\<open>Pure.all\<close> t')
     val objTs = map objT_of bounds
     val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty)
-  in Term_Subst.map_types (substTs_same subst) t' end
+  in Term.map_types (substTs_same subst) t' end
 
 fun eq_quant (\<^const_name>\<open>HOL.All\<close>, _) (\<^const_name>\<open>HOL.All\<close>, _) = true
   | eq_quant (\<^const_name>\<open>HOL.Ex\<close>, _) (\<^const_name>\<open>HOL.Ex\<close>, _) = true
diff -r d9cf62ea273d -r e1895596e1b9 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Dec 31 18:49:00 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Dec 31 19:24:37 2023 +0100
@@ -74,7 +74,7 @@
   | alternative _ NONE NONE = NONE
 
 fun varify_nonfixed_terms_global nonfixeds tm =
-  tm |> Term_Subst.map_aterms
+  tm |> Term.map_aterms
     (fn Free (x, T) => if member (op =) nonfixeds x then Var ((x, 0), T) else raise Same.SAME
       | Var (xi, _) => raise TERM (Logic.bad_schematic xi, [tm])
       | _ => raise Same.SAME)
diff -r d9cf62ea273d -r e1895596e1b9 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Dec 31 19:24:37 2023 +0100
@@ -390,7 +390,7 @@
     val cs = maps (fn T => map (pair T) S) Ts;
     val constraints' = map Logic.mk_of_class cs;
     val typ_map = Type.strip_sorts o
-      Term_Subst.map_atypsT (fn U =>
+      Term.map_atyps (fn U =>
         if member (op =) atyps U
         then #typ_operation ucontext {strip_sorts = false} U
         else raise Same.SAME);
diff -r d9cf62ea273d -r e1895596e1b9 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/envir.ML	Sun Dec 31 19:24:37 2023 +0100
@@ -341,14 +341,14 @@
 
 local
 
-fun subst_type0 tyenv = Term_Subst.map_atypsT_same
+fun subst_type0 tyenv = Term.map_atyps_same
   (fn TVar v =>
         (case Type.lookup tyenv v of
           SOME U => U
         | NONE => raise Same.SAME)
     | _ => raise Same.SAME);
 
-fun subst_term1 tenv = Term_Subst.map_aterms_same
+fun subst_term1 tenv = Term.map_aterms_same
   (fn Var v =>
         (case lookup1 tenv v of
           SOME u => u
@@ -381,7 +381,7 @@
 
 fun subst_term_types_same tyenv =
   if Vartab.is_empty tyenv then Same.same
-  else Term_Subst.map_types_same (subst_type0 tyenv);
+  else Term.map_types_same (subst_type0 tyenv);
 
 fun subst_term_same (tyenv, tenv) =
   if Vartab.is_empty tenv then subst_term_types_same tyenv
diff -r d9cf62ea273d -r e1895596e1b9 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/logic.ML	Sun Dec 31 19:24:37 2023 +0100
@@ -388,7 +388,7 @@
               SOME T' => T' |> strip_sorts ? Type.strip_sorts
             | NONE => raise TYPE ("Dangling type variable ", [T], [prop]))));
 
-    val typ_operation = Term_Subst.map_atypsT_same o atyp_operation;
+    val typ_operation = Term.map_atyps_same o atyp_operation;
 
     val constraints =
       constraints_map |> maps (fn (_, T as TVar (ai, S)) =>
@@ -402,7 +402,7 @@
       constraints = constraints,
       outer_constraints = outer_constraints};
     val prop' = prop
-      |> Term_Subst.map_types (typ_operation {strip_sorts = true})
+      |> Term.map_types (typ_operation {strip_sorts = true})
       |> curry list_implies (map #2 constraints);
   in (ucontext, prop') end;
 
@@ -447,7 +447,7 @@
   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
 
 fun incr_tvar_same 0 = Same.same
-  | incr_tvar_same inc = Term_Subst.map_atypsT_same
+  | incr_tvar_same inc = Term.map_atyps_same
       (fn TVar ((a, i), S) => TVar ((a, i + inc), S)
         | _ => raise Same.SAME);
 
@@ -612,12 +612,12 @@
 fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
 
 fun varifyT_global_same ty = ty
-  |> Term_Subst.map_atypsT_same
+  |> Term.map_atyps_same
     (fn TFree (a, S) => TVar ((a, 0), S)
       | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
 
 fun unvarifyT_global_same ty = ty
-  |> Term_Subst.map_atypsT_same
+  |> Term.map_atyps_same
     (fn TVar ((a, 0), S) => TFree (a, S)
       | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
       | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
@@ -626,22 +626,22 @@
 val unvarifyT_global = Same.commit unvarifyT_global_same;
 
 fun varify_types_global tm =
-  Term_Subst.map_types varifyT_global_same tm
+  Term.map_types varifyT_global_same tm
     handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
 
 fun unvarify_types_global tm =
-  Term_Subst.map_types unvarifyT_global_same tm
+  Term.map_types unvarifyT_global_same tm
     handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
 
 fun varify_global tm = tm
-  |> Term_Subst.map_aterms
+  |> Term.map_aterms
     (fn Free (x, T) => Var ((x, 0), T)
       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
       | _ => raise Same.SAME)
   |> varify_types_global;
 
 fun unvarify_global tm = tm
-  |> Term_Subst.map_aterms
+  |> Term.map_aterms
     (fn Var ((x, 0), T) => Free (x, T)
       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
       | Free (x, _) => raise TERM (bad_fixed x, [tm])
diff -r d9cf62ea273d -r e1895596e1b9 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/proofterm.ML	Sun Dec 31 19:24:37 2023 +0100
@@ -552,7 +552,7 @@
   in proof end;
 
 fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => PClass (typ T, c));
-fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ;
+fun map_proof_types_same typ = map_proof_terms_same (Term.map_types_same typ) typ;
 
 fun map_proof_terms f g =
   Same.commit (map_proof_terms_same (Same.function_eq (op =) f) (Same.function_eq (op =) g));
@@ -925,7 +925,7 @@
     let
       val tab = TFrees.make names;
       val typ =
-        Term_Subst.map_atypsT_same
+        Term.map_atyps_same
           (fn TFree v =>
               (case TFrees.lookup tab v of
                 NONE => raise Same.SAME
@@ -1118,7 +1118,7 @@
       let val T' = Same.commit typ_sort T
       in the_single (of_sort_proof algebra sorts_proof hyps (T', [c])) end;
   in
-    Same.commit (map_proof_same (Term_Subst.map_types_same typ) typ class)
+    Same.commit (map_proof_same (Term.map_types_same typ) typ class)
     #> fold_rev (implies_intr_proof o #2) (#constraints ucontext)
   end;
 
@@ -1613,7 +1613,7 @@
     fun subst_same A =
       (case AList.lookup (op =) inst A of SOME T => T | NONE => raise Same.SAME);
     val subst_type_same =
-      Term_Subst.map_atypsT_same
+      Term.map_atyps_same
         (fn TVar ((a, i), S) => subst_same (TVar ((a, i - shift), S)) | A => subst_same A);
   in Same.commit (map_proof_types_same subst_type_same) prf end;
 
@@ -2240,7 +2240,7 @@
     val proof2 =
       if unconstrain then
         proof_combt' (head,
-          (Same.commit o Same.map o Same.map_option o Term_Subst.map_types_same)
+          (Same.commit o Same.map o Same.map_option o Term.map_types_same)
             (typ_operation {strip_sorts = true}) args)
       else
         proof_combP (proof_combt' (head, args),
diff -r d9cf62ea273d -r e1895596e1b9 src/Pure/term.ML
--- a/src/Pure/term.ML	Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/term.ML	Sun Dec 31 19:24:37 2023 +0100
@@ -68,11 +68,11 @@
   val head_of: term -> term
   val size_of_term: term -> int
   val size_of_typ: typ -> int
-  val map_atyps: (typ -> typ) -> typ -> typ
-  val map_aterms: (term -> term) -> term -> term
-  val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
-  val map_type_tfree: (string * sort -> typ) -> typ -> typ
-  val map_types: (typ -> typ) -> term -> term
+  val map_atyps: typ Same.operation -> typ -> typ
+  val map_aterms: term Same.operation -> term -> term
+  val map_types: typ Same.operation -> term -> term
+  val map_type_tvar: (indexname * sort, typ) Same.function -> typ -> typ
+  val map_type_tfree: (string * sort, typ) Same.function -> typ -> typ
   val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
   val fold_atyps_sorts: (typ * sort -> 'a -> 'a) -> typ -> 'a -> 'a
   val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
@@ -122,6 +122,9 @@
 signature TERM =
 sig
   include BASIC_TERM
+  val map_atyps_same: typ Same.operation -> typ Same.operation
+  val map_aterms_same: term Same.operation -> term Same.operation
+  val map_types_same: typ Same.operation -> term Same.operation
   val aT: sort -> typ
   val itselfT: typ -> typ
   val a_itselfT: typ
@@ -449,25 +452,44 @@
       | add_size _ n = n + 1;
   in add_size ty 0 end;
 
-fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
-  | map_atyps f T = f T;
+
+(* map types and terms *)
+
+fun map_atyps_same f =
+  let
+    fun typ (Type (a, Ts)) = Type (a, Same.map typ Ts)
+      | typ T = f T;
+  in typ end;
 
-fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u
-  | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
-  | map_aterms f t = f t;
-
-fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
-fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
+fun map_aterms_same f =
+  let
+    fun term (Abs (x, T, t)) = Abs (x, T, term t)
+      | term (t $ u) =
+          (term t $ Same.commit term u
+            handle Same.SAME => t $ term u)
+      | term a = f a;
+  in term end;
 
-fun map_types f =
+fun map_types_same f =
   let
-    fun map_aux (Const (a, T)) = Const (a, f T)
-      | map_aux (Free (a, T)) = Free (a, f T)
-      | map_aux (Var (v, T)) = Var (v, f T)
-      | map_aux (Bound i) = Bound i
-      | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
-      | map_aux (t $ u) = map_aux t $ map_aux u;
-  in map_aux end;
+    fun term (Const (a, T)) = Const (a, f T)
+      | term (Free (a, T)) = Free (a, f T)
+      | term (Var (xi, T)) = Var (xi, f T)
+      | term (Bound _) = raise Same.SAME
+      | term (Abs (x, T, t)) =
+          (Abs (x, f T, Same.commit term t)
+            handle Same.SAME => Abs (x, T, term t))
+      | term (t $ u) =
+          (term t $ Same.commit term u
+            handle Same.SAME => t $ term u);
+  in term end;
+
+val map_atyps = Same.commit o map_atyps_same;
+val map_aterms = Same.commit o map_aterms_same;
+val map_types = Same.commit o map_types_same;
+
+fun map_type_tvar f = map_atyps (fn TVar x => f x | _ => raise Same.SAME);
+fun map_type_tfree f = map_atyps (fn TFree x => f x | _ => raise Same.SAME);
 
 
 (* fold types and terms *)
diff -r d9cf62ea273d -r e1895596e1b9 src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/term_subst.ML	Sun Dec 31 19:24:37 2023 +0100
@@ -6,12 +6,6 @@
 
 signature TERM_SUBST =
 sig
-  val map_atypsT_same: typ Same.operation -> typ Same.operation
-  val map_types_same: typ Same.operation -> term Same.operation
-  val map_aterms_same: term Same.operation -> term Same.operation
-  val map_atypsT: typ Same.operation -> typ -> typ
-  val map_types: typ Same.operation -> term -> term
-  val map_aterms: term Same.operation -> term -> term
   val generalizeT_same: Names.set -> int -> typ Same.operation
   val generalize_same: Names.set * Names.set -> int -> term Same.operation
   val generalizeT: Names.set -> int -> typ -> typ
@@ -39,38 +33,6 @@
 structure Term_Subst: TERM_SUBST =
 struct
 
-(* generic mapping *)
-
-fun map_atypsT_same f =
-  let
-    fun typ (Type (a, Ts)) = Type (a, Same.map typ Ts)
-      | typ T = f T;
-  in typ end;
-
-fun map_types_same f =
-  let
-    fun term (Const (a, T)) = Const (a, f T)
-      | term (Free (a, T)) = Free (a, f T)
-      | term (Var (v, T)) = Var (v, f T)
-      | term (Bound _) = raise Same.SAME
-      | term (Abs (x, T, t)) =
-          (Abs (x, f T, Same.commit term t)
-            handle Same.SAME => Abs (x, T, term t))
-      | term (t $ u) = (term t $ Same.commit term u handle Same.SAME => t $ term u);
-  in term end;
-
-fun map_aterms_same f =
-  let
-    fun term (Abs (x, T, t)) = Abs (x, T, term t)
-      | term (t $ u) = (term t $ Same.commit term u handle Same.SAME => t $ term u)
-      | term a = f a;
-  in term end;
-
-val map_atypsT = Same.commit o map_atypsT_same;
-val map_types = Same.commit o map_types_same;
-val map_aterms = Same.commit o map_aterms_same;
-
-
 (* generalization of fixed variables *)
 
 fun generalizeT_same tfrees idx ty =
diff -r d9cf62ea273d -r e1895596e1b9 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/thm.ML	Sun Dec 31 19:24:37 2023 +0100
@@ -1102,7 +1102,7 @@
             (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar));
 
         val zproof' = ZTerm.map_proof_types map_ztyp zproof;
-        val proof' = Proofterm.map_proof_types (Term_Subst.map_atypsT_same map_atyp) proof;
+        val proof' = Proofterm.map_proof_types (Term.map_atyps_same map_atyp) proof;
       in
         Thm (make_deriv promises oracles thms zboxes zproof' proof',
          {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints',
diff -r d9cf62ea273d -r e1895596e1b9 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/type_infer.ML	Sun Dec 31 19:24:37 2023 +0100
@@ -48,7 +48,7 @@
 fun anyT S = TFree ("'_dummy_", S);
 
 val paramify_vars =
-  Term_Subst.map_atypsT (fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME);
+  Term.map_atyps (fn TVar ((x, i), S) => param i (x, S) | _ => raise Same.SAME);