# HG changeset patch
# User wenzelm
# Date 1704818330 -3600
# Node ID 6b6e9af552f5a875aa4a5d0c132038c618dfa876
# Parent  fe0fffc5d18660317b99fb215d97c7c620800bea
clarified signature: avoid redundant Term.maxidx_of_term;

diff -r fe0fffc5d186 -r 6b6e9af552f5 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Jan 09 17:25:43 2024 +0100
+++ b/src/Pure/sign.ML	Tue Jan 09 17:38:50 2024 +0100
@@ -65,8 +65,8 @@
   val certify_typ: theory -> typ -> typ
   val certify_typ_mode: Type.mode -> theory -> typ -> typ
   val certify_flags: {prop: bool, do_expand: bool} -> Context.generic -> Consts.T -> theory ->
-    term -> term * typ * int
-  val certify_term: theory -> term -> term * typ * int
+    term -> term * typ
+  val certify_term: theory -> term -> term * typ
   val cert_term: theory -> term -> term
   val cert_prop: theory -> term -> term
   val no_frees: Proof.context -> term -> term
@@ -319,7 +319,7 @@
     val (tm1, ty1) = check_term tm;
     val tm' = Soft_Type_System.global_purge thy tm1;
     val (tm2, ty2) = if tm1 = tm' then (tm1, ty1) else check_term tm';
-  in (if tm = tm2 then tm else tm2, ty2, Term.maxidx_of_term tm2) end;
+  in if tm = tm2 then (tm, ty2) else (tm2, ty2) end;
 
 fun certify_term thy =
   certify_flags {prop = false, do_expand = true} (Context.Theory thy) (consts_of thy) thy;
diff -r fe0fffc5d186 -r 6b6e9af552f5 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Jan 09 17:25:43 2024 +0100
+++ b/src/Pure/thm.ML	Tue Jan 09 17:38:50 2024 +0100
@@ -269,7 +269,8 @@
 
 fun global_cterm_of thy tm =
   let
-    val (t, T, maxidx) = Sign.certify_term thy tm;
+    val (t, T) = Sign.certify_term thy tm;
+    val maxidx = Term.maxidx_of_term t;
     val sorts = Sorts.insert_term t [];
   in Cterm {cert = Context.Certificate thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;