# HG changeset patch
# User wenzelm
# Date 1704799081 -3600
# Node ID e6fb110d6e4452e6f7b70cb6baf2c1a443c608e5
# Parent  a5f327d9466f7baabf79faa52948c18789bdb317
clarified signature;

diff -r a5f327d9466f -r e6fb110d6e44 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jan 09 12:06:07 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Jan 09 12:18:01 2024 +0100
@@ -495,7 +495,7 @@
 
 
 fun cert_typ_mode mode ctxt T =
-  Type.cert_typ_mode mode (tsig_of ctxt) T
+  Type.cert_typ mode (tsig_of ctxt) T
     handle TYPE (msg, _, _) => error msg;
 
 val cert_typ = cert_typ_mode Type.mode_default;
diff -r a5f327d9466f -r e6fb110d6e44 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Tue Jan 09 12:06:07 2024 +0100
+++ b/src/Pure/consts.ML	Tue Jan 09 12:18:01 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 = Type.cert_typ tsig;
+    val certT = Type.cert_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 tsig)
+      |> Term.map_types (Type.cert_typ Type.mode_default tsig)
       |> cert_term
       |> Term.close_schematic_term;
     val normal_rhs = expand_term rhs;
diff -r a5f327d9466f -r e6fb110d6e44 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Jan 09 12:06:07 2024 +0100
+++ b/src/Pure/sign.ML	Tue Jan 09 12:18:01 2024 +0100
@@ -259,8 +259,8 @@
 
 val certify_class = Type.cert_class o tsig_of;
 val certify_sort = Type.cert_sort o tsig_of;
-val certify_typ = Type.cert_typ o tsig_of;
-fun certify_typ_mode mode = Type.cert_typ_mode mode o tsig_of;
+val certify_typ = Type.cert_typ Type.mode_default o tsig_of;
+fun certify_typ_mode mode = Type.cert_typ mode o tsig_of;
 
 
 (* certify term/prop *)
diff -r a5f327d9466f -r e6fb110d6e44 src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Jan 09 12:06:07 2024 +0100
+++ b/src/Pure/type.ML	Tue Jan 09 12:18:01 2024 +0100
@@ -53,8 +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_mode: mode -> tsig -> typ -> typ
-  val cert_typ: tsig -> typ -> typ
+  val cert_typ: mode -> tsig -> typ -> typ
   val arity_number: tsig -> string -> int
   val arity_sorts: Context.generic -> tsig -> string -> sort -> sort list
 
@@ -272,7 +271,7 @@
 
 in
 
-fun cert_typ_mode (Mode {normalize, logical}) tsig ty =
+fun cert_typ (Mode {normalize, logical}) tsig ty =
   let
     fun err msg = raise TYPE (msg, [ty], []);
 
@@ -303,8 +302,6 @@
     val ty' = cert ty;
   in if ty = ty' then ty else ty' end;  (*avoid copying of already normal type*)
 
-val cert_typ = cert_typ_mode mode_default;
-
 end;
 
 
@@ -694,7 +691,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 (cert_typ_mode mode_syntax tsig rhs))
+    val rhs' = Term.strip_sortsT (no_tvars (cert_typ mode_syntax tsig rhs))
       handle TYPE (msg, _, _) => err msg;
     val _ =
       (case duplicates (op =) vs of