# HG changeset patch
# User wenzelm
# Date 1704888620 -3600
# Node ID 7d10708bbc32c5904bea572a84222fedfaca2a31
# Parent  fbdffff89f99229fba6035b3f76e43f491678ba8
clarified signature;

diff -r fbdffff89f99 -r 7d10708bbc32 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jan 10 11:39:01 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Jan 10 13:10:20 2024 +0100
@@ -584,7 +584,7 @@
     val _ =
       (case (strict, t) of
         (true, Const (d, _)) =>
-          (ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg)
+          (ignore (Consts.the_const_type consts d) handle TYPE (msg, _, _) => err msg)
       | _ => ());
   in (t, reports) end;
 
diff -r fbdffff89f99 -r 7d10708bbc32 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Wed Jan 10 11:39:01 2024 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Wed Jan 10 13:10:20 2024 +0100
@@ -150,7 +150,7 @@
 
 val _ = Theory.setup
  (ML_Antiquotation.inline_embedded \<^binding>\<open>const_name\<close>
-    (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
+    (const_name (fn (consts, c) => (Consts.the_const_type consts c; c))) #>
   ML_Antiquotation.inline_embedded \<^binding>\<open>const_abbrev\<close>
     (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
   ML_Antiquotation.inline_embedded \<^binding>\<open>const_syntax\<close>
diff -r fbdffff89f99 -r 7d10708bbc32 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Wed Jan 10 11:39:01 2024 +0100
+++ b/src/Pure/consts.ML	Wed Jan 10 13:10:20 2024 +0100
@@ -17,7 +17,7 @@
     constants: (string * (typ * term option)) list,
     constraints: (string * typ) list}
   val get_const_name: T -> string -> string option
-  val the_const: T -> string -> string * typ                   (*exception TYPE*)
+  val the_const_type: T -> string -> typ                       (*exception TYPE*)
   val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
   val type_scheme: T -> string -> typ                          (*exception TYPE*)
   val type_arguments: T -> string -> int list list             (*exception TYPE*)
@@ -117,9 +117,9 @@
     SOME entry => entry
   | NONE => raise TYPE ("Unknown constant: " ^ quote c, [], []));
 
-fun the_const consts c =
+fun the_const_type consts c =
   (case the_entry consts c of
-    (c', ({T, ...}, NONE)) => (c', T)
+    (_, ({T, ...}, NONE)) => T
   | _ => raise TYPE ("Not a logical constant: " ^ quote c, [], []));
 
 fun the_abbreviation consts c =
diff -r fbdffff89f99 -r 7d10708bbc32 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Jan 10 11:39:01 2024 +0100
+++ b/src/Pure/sign.ML	Wed Jan 10 13:10:20 2024 +0100
@@ -207,7 +207,7 @@
 
 val consts_of = #consts o rep_sg;
 val the_const_constraint = Consts.the_constraint o consts_of;
-val the_const_type = #2 oo (Consts.the_const o consts_of);
+val the_const_type = Consts.the_const_type o consts_of;
 val const_type = try o the_const_type;
 val const_monomorphic = Consts.is_monomorphic o consts_of;
 val const_typargs = Consts.typargs o consts_of;