# HG changeset patch
# User wenzelm
# Date 1704882816 -3600
# Node ID 5f49d9d1bb195e71bb42ba4cbef4c4c7f1542a9e
# Parent  094eb331ebbf01630be7a67e122e24d059c3d097
tuned signature;

diff -r 094eb331ebbf -r 5f49d9d1bb19 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Wed Jan 10 11:28:20 2024 +0100
+++ b/src/Pure/consts.ML	Wed Jan 10 11:33:36 2024 +0100
@@ -209,7 +209,7 @@
         | _ => comb head)
       end;
 
-    val typ = Type.cert_typ_same Type.mode_default tsig;
+    val typ = Type.certify_typ_same Type.mode_default tsig;
     fun term (Const (c, T)) =
           let
             val (T', same) = Same.commit_id typ T;
diff -r 094eb331ebbf -r 5f49d9d1bb19 src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Jan 10 11:28:20 2024 +0100
+++ b/src/Pure/type.ML	Wed Jan 10 11:33:36 2024 +0100
@@ -53,7 +53,7 @@
   val check_decl: Context.generic -> tsig ->
     xstring * Position.T -> (string * Position.report list) * decl
   val the_decl: tsig -> string * Position.T -> decl
-  val cert_typ_same: mode -> tsig -> typ Same.operation
+  val certify_typ_same: mode -> tsig -> typ Same.operation
   val certify_typ: mode -> tsig -> typ -> typ
   val certify_types: mode -> tsig -> term -> term
   val arity_number: tsig -> string -> int
@@ -277,7 +277,7 @@
 
 in
 
-fun cert_typ_same (Mode {normalize, logical}) tsig =
+fun certify_typ_same (Mode {normalize, logical}) tsig =
   let
     fun err T msg = raise TYPE (msg, [T], []);
     fun err_syntactic T c = err T ("Illegal occurrence of syntactic type: " ^ quote c);
@@ -303,8 +303,8 @@
 
 end;
 
-val certify_typ = Same.commit oo cert_typ_same;
-val certify_types = Term.map_types oo cert_typ_same;
+val certify_typ = Same.commit oo certify_typ_same;
+val certify_types = Term.map_types oo certify_typ_same;
 
 
 (* type arities *)