clarified signature: more operations;

--- a/src/HOL/Tools/SMT/z3_proof.ML	Sat Dec 30 22:16:18 2023 +0100
+++ b/src/HOL/Tools/SMT/z3_proof.ML	Sat Dec 30 22:36:41 2023 +0100
@@ -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 Same.commit (Term_Subst.map_types_same (substTs_same subst)) t' end
+  in Term_Subst.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

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Dec 30 22:16:18 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Dec 30 22:36:41 2023 +0100
@@ -73,11 +73,11 @@
   | alternative _ NONE (y as SOME _) = y
   | alternative _ NONE NONE = NONE
 
-fun varify_nonfixed_terms_global nonfixeds tm = tm
-  |> Same.commit (Term_Subst.map_aterms_same
+fun varify_nonfixed_terms_global nonfixeds tm =
+  tm |> Term_Subst.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))
+      | _ => raise Same.SAME)
 
 fun max_outcome outcomes =
   let

--- a/src/Pure/Proof/extraction.ML	Sat Dec 30 22:16:18 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Sat Dec 30 22:36:41 2023 +0100
@@ -390,10 +390,10 @@
     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
-      Same.commit (Term_Subst.map_atypsT_same (fn U =>
+      Term_Subst.map_atypsT (fn U =>
         if member (op =) atyps U
         then #unconstrain_typ ucontext {strip_sorts = false} U
-        else raise Same.SAME));
+        else raise Same.SAME);
     fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c));
     val xs' = map (map_types typ_map) xs
   in

--- a/src/Pure/logic.ML	Sat Dec 30 22:16:18 2023 +0100
+++ b/src/Pure/logic.ML	Sat Dec 30 22:36:41 2023 +0100
@@ -404,7 +404,7 @@
       constraints = constraints,
       outer_constraints = outer_constraints};
     val prop' = prop
-      |> Same.commit (Term_Subst.map_types_same (unconstrain_typ {strip_sorts = true}))
+      |> Term_Subst.map_types (unconstrain_typ {strip_sorts = true})
       |> curry list_implies (map #2 constraints);
   in (ucontext, prop') end;
 
@@ -627,27 +627,27 @@
 val varifyT_global = Same.commit varifyT_global_same;
 val unvarifyT_global = Same.commit unvarifyT_global_same;
 
-fun varify_types_global tm = tm
-  |> Same.commit (Term_Subst.map_types_same varifyT_global_same)
-  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
+fun varify_types_global tm =
+  Term_Subst.map_types varifyT_global_same tm
+    handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
 
-fun unvarify_types_global tm = tm
-  |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same)
-  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
+fun unvarify_types_global tm =
+  Term_Subst.map_types unvarifyT_global_same tm
+    handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
 
 fun varify_global tm = tm
-  |> Same.commit (Term_Subst.map_aterms_same
+  |> Term_Subst.map_aterms
     (fn Free (x, T) => Var ((x, 0), T)
       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
-      | _ => raise Same.SAME))
+      | _ => raise Same.SAME)
   |> varify_types_global;
 
 fun unvarify_global tm = tm
-  |> Same.commit (Term_Subst.map_aterms_same
+  |> Term_Subst.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])
-      | _ => raise Same.SAME))
+      | _ => raise Same.SAME)
   |> unvarify_types_global;
 
 

--- a/src/Pure/term_subst.ML	Sat Dec 30 22:16:18 2023 +0100
+++ b/src/Pure/term_subst.ML	Sat Dec 30 22:36:41 2023 +0100
@@ -9,6 +9,9 @@
   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
@@ -63,6 +66,10 @@
       | 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 *)
 

--- a/src/Pure/type_infer.ML	Sat Dec 30 22:16:18 2023 +0100
+++ b/src/Pure/type_infer.ML	Sat Dec 30 22:36:41 2023 +0100
@@ -48,9 +48,7 @@
 fun anyT S = TFree ("'_dummy_", S);
 
 val paramify_vars =
-  Same.commit
-    (Term_Subst.map_atypsT_same
-      (fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME));
+  Term_Subst.map_atypsT (fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME);