tuned signature: more operations;

--- a/src/Pure/Isar/specification.ML	Sun Aug 04 13:24:54 2024 +0200
+++ b/src/Pure/Isar/specification.ML	Sun Aug 04 16:56:28 2024 +0200
@@ -319,7 +319,7 @@
 val alias_cmd =
   gen_alias Local_Theory.const_alias
     (fn flags => fn ctxt => fn (c, pos) =>
-      apfst (#1 o dest_Const) (Proof_Context.check_const flags ctxt (c, [pos])));
+      apfst dest_Const_name (Proof_Context.check_const flags ctxt (c, [pos])));
 
 val type_alias =
   gen_alias Local_Theory.type_alias (K (K (fn c => (c, []))));

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Sun Aug 04 13:24:54 2024 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sun Aug 04 16:56:28 2024 +0200
@@ -269,7 +269,7 @@
     val prf' =
       if r then
         let
-          val cnames = map (fst o dest_Const o fst) defs';
+          val cnames = map (dest_Const_name o fst) defs';
           val expand = Proofterm.fold_proof_atoms true
             (fn PThm ({serial, thm_name = (thm_name, _), prop, ...}, _) =>
                 if member (op =) defnames thm_name orelse

--- a/src/Pure/Pure.thy	Sun Aug 04 13:24:54 2024 +0200
+++ b/src/Pure/Pure.thy	Sun Aug 04 16:56:28 2024 +0200
@@ -609,7 +609,7 @@
 
 val _ =
   hide_names \<^command_keyword>\<open>hide_const\<close> "consts" Sign.hide_const Parse.const
-    ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
+    (dest_Const_name oo Proof_Context.read_const {proper = true, strict = false});
 
 val _ =
   hide_names \<^command_keyword>\<open>hide_fact\<close> "facts" Global_Theory.hide_fact

--- a/src/Pure/term.ML	Sun Aug 04 13:24:54 2024 +0200
+++ b/src/Pure/term.ML	Sun Aug 04 16:56:28 2024 +0200
@@ -47,6 +47,8 @@
   val is_Free: term -> bool
   val is_Var: term -> bool
   val dest_Const: term -> string * typ
+  val dest_Const_name: term -> string
+  val dest_Const_type: term -> typ
   val dest_Free: term -> string * typ
   val dest_Var: term -> indexname * typ
   val dest_comb: term -> term * term
@@ -314,6 +316,9 @@
 fun dest_Const (Const x) =  x
   | dest_Const t = raise TERM("dest_Const", [t]);
 
+val dest_Const_name = #1 o dest_Const;
+val dest_Const_type = #2 o dest_Const;
+
 fun dest_Free (Free x) =  x
   | dest_Free t = raise TERM("dest_Free", [t]);