# HG changeset patch
# User wenzelm
# Date 1704749164 -3600
# Node ID 739b1703866e3f6c727b3cf8ea3afe3365364532
# Parent  032ca41f590a03d13873be4bdbd568c6d35d7778
minor performance tuning;
eliminate clones;

diff -r 032ca41f590a -r 739b1703866e src/HOL/Tools/Nunchaku/nunchaku_collect.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Mon Jan 08 21:54:20 2024 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Mon Jan 08 22:26:04 2024 +0100
@@ -190,7 +190,7 @@
       raise UNEXPECTED_POLYMORPHISM t
     else
       t
-      |> attach_typeS
+      |> Term.smash_sorts \<^sort>\<open>type\<close>
       |> whack_term thy whacks
       |> Object_Logic.atomize_term ctxt
       |> tap (fn t' => fastype_of t' <> \<^typ>\<open>prop\<close> orelse raise TOO_META t)
diff -r 032ca41f590a -r 739b1703866e src/HOL/Tools/Nunchaku/nunchaku_util.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_util.ML	Mon Jan 08 21:54:20 2024 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_util.ML	Mon Jan 08 22:26:04 2024 +0100
@@ -23,7 +23,6 @@
   val with_tmp_or_overlord_file: bool -> string -> string -> (Path.T -> 'a) -> 'a
   val num_binder_types: typ -> int
   val strip_fun_type: typ -> typ list * typ
-  val attach_typeS: term -> term
   val specialize_type: theory -> string * typ -> term -> term
   val typ_match: theory -> typ * typ -> bool
   val term_match: theory -> term * term -> bool
@@ -58,13 +57,6 @@
 val num_binder_types = BNF_Util.num_binder_types
 val strip_fun_type = BNF_Util.strip_fun_type;
 
-(* Clone from "HOL/Tools/inductive_realizer.ML". *)
-val attach_typeS =
-  map_types (map_atyps
-    (fn TFree (s, []) => TFree (s, \<^sort>\<open>type\<close>)
-      | TVar (ixn, []) => TVar (ixn, \<^sort>\<open>type\<close>)
-      | T => T));
-
 val specialize_type = ATP_Util.specialize_type;
 
 fun typ_match thy TU = can (Sign.typ_match thy TU) Vartab.empty;
diff -r 032ca41f590a -r 739b1703866e src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Mon Jan 08 21:54:20 2024 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon Jan 08 22:26:04 2024 +0100
@@ -52,10 +52,7 @@
         (_, Type (s, _)) => if s = \<^type_name>\<open>bool\<close> then (a, T) :: vs else vs
       | _ => vs)) (Term.add_vars prop []) [];
 
-val attach_typeS = map_types (map_atyps
-  (fn TFree (s, []) => TFree (s, \<^sort>\<open>type\<close>)
-    | TVar (ixn, []) => TVar (ixn, \<^sort>\<open>type\<close>)
-    | T => T));
+val attach_typeS = Term.smash_sorts \<^sort>\<open>type\<close>;
 
 fun dt_of_intrs thy vs nparms intrs =
   let
diff -r 032ca41f590a -r 739b1703866e src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Jan 08 21:54:20 2024 +0100
+++ b/src/Pure/Isar/class.ML	Mon Jan 08 22:26:04 2024 +0100
@@ -190,7 +190,7 @@
         val Ss = Sorts.mg_domain algebra tyco [class];
       in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
 
-    fun prt_param (c, ty) = pretty_param ctxt (c, Same.commit (Term.smash_sortsT_same dummyS) ty);
+    fun prt_param (c, ty) = pretty_param ctxt (c, Term.smash_sortsT dummyS ty);
 
     fun prt_entry class =
       Pretty.block
@@ -245,10 +245,11 @@
 fun register_operation class (c, t) input_only thy =
   let
     val base_sort = base_sort thy class;
-    val prep_typ = map_type_tfree
-      (fn (v, sort) => if Name.aT = v
-        then TFree (v, base_sort) else TVar ((v, 0), sort));
-    val t' = map_types prep_typ t;
+    val prep_types =
+      (Same.commit o Term.map_types_same o Term.map_atyps_same)
+        (fn TFree (v, S) => if Name.aT = v then TFree (v, base_sort) else TVar ((v, 0), S)
+          | _ => raise Same.SAME);
+    val t' = prep_types t;
     val ty' = Term.fastype_of t';
   in
     thy
diff -r 032ca41f590a -r 739b1703866e src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Jan 08 21:54:20 2024 +0100
+++ b/src/Pure/term.ML	Mon Jan 08 22:26:04 2024 +0100
@@ -151,6 +151,8 @@
   val declare_term_frees: term -> Name.context -> Name.context
   val variant_frees: term -> (string * 'a) list -> (string * 'a) list
   val smash_sortsT_same: sort -> typ Same.operation
+  val smash_sortsT: sort -> typ -> typ
+  val smash_sorts: sort -> term -> term
   val strip_sortsT_same: typ Same.operation
   val strip_sortsT: typ -> typ
   val strip_sorts: term -> term
@@ -590,6 +592,9 @@
     (fn TFree (x, S) => if S = S' then raise Same.SAME else TFree (x, S')
       | TVar (xi, S) => if S = S' then raise Same.SAME else TVar (xi, S'));
 
+val smash_sortsT = Same.commit o smash_sortsT_same;
+val smash_sorts = map_types o smash_sortsT_same;
+
 val strip_sortsT_same = smash_sortsT_same [];
 val strip_sortsT = Same.commit strip_sortsT_same;
 val strip_sorts = map_types strip_sortsT_same;