src/Pure/sign.ML

--- a/src/Pure/sign.ML	Tue Jan 09 17:38:50 2024 +0100
+++ b/src/Pure/sign.ML	Tue Jan 09 22:40:38 2024 +0100
@@ -260,7 +260,7 @@
 
 val certify_class = Type.cert_class o tsig_of;
 val certify_sort = Type.cert_sort o tsig_of;
-fun certify_typ_mode mode thy = Same.commit (Type.cert_typ_same mode (tsig_of thy));
+fun certify_typ_mode mode = Type.certify_typ mode o tsig_of;
 val certify_typ = certify_typ_mode Type.mode_default;
 
 
@@ -311,7 +311,7 @@
     fun check_term t =
       let
         val _ = check_vars t;
-        val t' = Term.map_types (Type.cert_typ_same Type.mode_default tsig) t;
+        val t' = Type.certify_types Type.mode_default tsig t;
         val T = type_check context t';
         val t'' = Consts.certify {do_expand = do_expand} context tsig consts t';
       in if prop andalso T <> propT then err "Term not of type prop" else (t'', T) end;