# HG changeset patch
# User wenzelm
# Date 1704836438 -3600
# Node ID d7f32f04bd1343549ee5d82b42f336a4129e7d2b
# Parent  6b6e9af552f5a875aa4a5d0c132038c618dfa876
clarified signature;

diff -r 6b6e9af552f5 -r d7f32f04bd13 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jan 09 17:38:50 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Jan 09 22:40:38 2024 +0100
@@ -495,7 +495,7 @@
 
 
 fun cert_typ_mode mode ctxt T =
-  Same.commit (Type.cert_typ_same mode (tsig_of ctxt)) T
+  Type.certify_typ mode (tsig_of ctxt) T
     handle TYPE (msg, _, _) => error msg;
 
 val cert_typ = cert_typ_mode Type.mode_default;
diff -r 6b6e9af552f5 -r d7f32f04bd13 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Tue Jan 09 17:38:50 2024 +0100
+++ b/src/Pure/consts.ML	Tue Jan 09 22:40:38 2024 +0100
@@ -169,7 +169,7 @@
     fun err msg (c, T) =
       raise TYPE (msg ^ " " ^ quote c ^ " :: " ^
         Syntax.string_of_typ (Syntax.init_pretty context) T, [], []);
-    val certT = Same.commit (Type.cert_typ_same Type.mode_default tsig);
+    val certT = Type.certify_typ Type.mode_default tsig;
     fun cert tm =
       let
         val (head, args) = Term.strip_comb tm;
@@ -301,7 +301,7 @@
       error ("Illegal schematic variables on rhs of abbreviation " ^ Binding.print b);
 
     val rhs = raw_rhs
-      |> Term.map_types (Type.cert_typ_same Type.mode_default tsig)
+      |> Type.certify_types Type.mode_default tsig
       |> cert_term
       |> Term.close_schematic_term;
     val normal_rhs = expand_term rhs;
diff -r 6b6e9af552f5 -r d7f32f04bd13 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;
diff -r 6b6e9af552f5 -r d7f32f04bd13 src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Jan 09 17:38:50 2024 +0100
+++ b/src/Pure/type.ML	Tue Jan 09 22:40:38 2024 +0100
@@ -54,6 +54,8 @@
     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: mode -> tsig -> typ -> typ
+  val certify_types: mode -> tsig -> term -> term
   val arity_number: tsig -> string -> int
   val arity_sorts: Context.generic -> tsig -> string -> sort -> sort list
 
@@ -263,7 +265,7 @@
   | SOME decl => decl);
 
 
-(* certified types *)
+(* certify types *)
 
 fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t;
 
@@ -301,6 +303,9 @@
 
 end;
 
+val certify_typ = Same.commit oo cert_typ_same;
+val certify_types = Term.map_types oo cert_typ_same;
+
 
 (* type arities *)
 
@@ -688,7 +693,7 @@
   let
     fun err msg =
       cat_error msg ("The error(s) above occurred in type abbreviation " ^ Binding.print a);
-    val rhs' = Term.strip_sortsT (no_tvars (Same.commit (cert_typ_same mode_syntax tsig) rhs))
+    val rhs' = Term.strip_sortsT (no_tvars (certify_typ mode_syntax tsig rhs))
       handle TYPE (msg, _, _) => err msg;
     val _ =
       (case duplicates (op =) vs of