tuned signature: more operations;

--- a/src/Pure/Isar/isar_cmd.ML	Sat Aug 03 13:12:58 2024 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Aug 04 12:21:13 2024 +0200
@@ -98,7 +98,7 @@
   let
     val ctxt = Proof_Context.init_global thy;
     val read_root =
-      #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} ctxt;
+      dest_Type_name o Proof_Context.read_type_name {proper = true, strict = false} ctxt;
   in
     raw_rules
     |> map (Syntax.map_trrule (fn (r, s) => Syntax_Phases.parse_ast_pattern ctxt (read_root r, s)))

--- a/src/Pure/Isar/proof_context.ML	Sat Aug 03 13:12:58 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Aug 04 12:21:13 2024 +0200
@@ -608,7 +608,7 @@
 in
 
 val read_arity =
-  prep_arity ((#1 o dest_Type) oo read_type_name {proper = true, strict = true}) Syntax.read_sort;
+  prep_arity (dest_Type_name oo read_type_name {proper = true, strict = true}) Syntax.read_sort;
 
 val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
 

--- a/src/Pure/Isar/specification.ML	Sat Aug 03 13:12:58 2024 +0200
+++ b/src/Pure/Isar/specification.ML	Sun Aug 04 12:21:13 2024 +0200
@@ -324,7 +324,7 @@
 val type_alias =
   gen_alias Local_Theory.type_alias (K (K (fn c => (c, []))));
 val type_alias_cmd =
-  gen_alias Local_Theory.type_alias (apfst (#1 o dest_Type) ooo Proof_Context.check_type_name);
+  gen_alias Local_Theory.type_alias (apfst dest_Type_name ooo Proof_Context.check_type_name);
 
 
 (* fact statements *)

--- a/src/Pure/Isar/typedecl.ML	Sat Aug 03 13:12:58 2024 +0200
+++ b/src/Pure/Isar/typedecl.ML	Sun Aug 04 12:21:13 2024 +0200
@@ -50,7 +50,7 @@
     val T = Type (Local_Theory.full_name lthy b, args);
 
     val bad_args =
-      #2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T))
+      Term.dest_Type_args (Logic.type_map (singleton (Variable.polymorphic lthy)) T)
       |> filter_out Term.is_TVar;
     val _ = null bad_args orelse
       err ("Locally fixed type arguments " ^

--- a/src/Pure/Pure.thy	Sat Aug 03 13:12:58 2024 +0200
+++ b/src/Pure/Pure.thy	Sun Aug 04 12:21:13 2024 +0200
@@ -605,7 +605,7 @@
 
 val _ =
   hide_names \<^command_keyword>\<open>hide_type\<close> "types" Sign.hide_type Parse.type_const
-    ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
+    (dest_Type_name oo Proof_Context.read_type_name {proper = true, strict = false});
 
 val _ =
   hide_names \<^command_keyword>\<open>hide_const\<close> "consts" Sign.hide_const Parse.const

--- a/src/Pure/axclass.ML	Sat Aug 03 13:12:58 2024 +0200
+++ b/src/Pure/axclass.ML	Sun Aug 04 12:21:13 2024 +0200
@@ -164,7 +164,7 @@
     (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of (Proof_Context.theory_of ctxt))) []
   |> map (Thm.transfer' ctxt);
 
-fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts);
+fun get_inst_tyco consts = try (dest_Type_name o the_single o Consts.typargs consts);
 
 fun unoverload ctxt = rewrite_rule ctxt (inst_thms ctxt);
 fun overload ctxt = rewrite_rule ctxt (map Thm.symmetric (inst_thms ctxt));

--- a/src/Pure/term.ML	Sat Aug 03 13:12:58 2024 +0200
+++ b/src/Pure/term.ML	Sun Aug 04 12:21:13 2024 +0200
@@ -38,6 +38,8 @@
   val is_TFree: typ -> bool
   val is_TVar: typ -> bool
   val dest_Type: typ -> string * typ list
+  val dest_Type_name: typ -> string
+  val dest_Type_args: typ -> typ list
   val dest_TFree: typ -> string * sort
   val dest_TVar: typ -> indexname * sort
   val is_Bound: term -> bool
@@ -282,6 +284,9 @@
 fun dest_Type (Type x) = x
   | dest_Type T = raise TYPE ("dest_Type", [T], []);
 
+val dest_Type_name = #1 o dest_Type;
+val dest_Type_args = #2 o dest_Type;
+
 fun dest_TFree (TFree x) = x
   | dest_TFree T = raise TYPE ("dest_TFree", [T], []);