--- 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;
--- 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 *)