# HG changeset patch
# User wenzelm
# Date 1704797836 -3600
# Node ID 57d29f537723541807d3c6db3d7ff53a6a9f7b97
# Parent  ec7a1603129a38473a756e89ee291fab5904d959
clarified modules;
minor performance tuning;

diff -r ec7a1603129a -r 57d29f537723 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Tue Jan 09 11:54:36 2024 +0100
+++ b/src/Pure/sorts.ML	Tue Jan 09 11:57:16 2024 +0100
@@ -30,6 +30,8 @@
   val arities_of: algebra -> (class * sort list) list Symtab.table
   val all_classes: algebra -> class list
   val super_classes: algebra -> class -> class list
+  val cert_class: algebra -> class -> class
+  val cert_sort: algebra -> sort -> sort
   val class_less: algebra -> class * class -> bool
   val class_le: algebra -> class * class -> bool
   val sort_eq: algebra -> sort * sort -> bool
@@ -135,6 +137,12 @@
 
 val super_classes = Graph.immediate_succs o classes_of;
 
+fun cert_class (Algebra {classes, ...}) c =
+  if Graph.defined classes c then c
+  else raise TYPE ("Undeclared class: " ^ quote c, [], []);
+
+fun cert_sort algebra S = (List.app (ignore o cert_class algebra) S; S);
+
 
 (* class relations *)
 
diff -r ec7a1603129a -r 57d29f537723 src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Jan 09 11:54:36 2024 +0100
+++ b/src/Pure/type.ML	Tue Jan 09 11:57:16 2024 +0100
@@ -211,11 +211,8 @@
 fun of_sort (TSig {classes, ...}) = Sorts.of_sort (#2 classes);
 fun inter_sort (TSig {classes, ...}) = Sorts.inter_sort (#2 classes);
 
-fun cert_class (TSig {classes = (_, algebra), ...}) c =
-  if can (Graph.get_entry (Sorts.classes_of algebra)) c then c
-  else raise TYPE ("Undeclared class: " ^ quote c, [], []);
-
-val cert_sort = map o cert_class;
+fun cert_class (TSig {classes, ...}) = Sorts.cert_class (#2 classes);
+fun cert_sort (TSig {classes, ...}) = Sorts.cert_sort (#2 classes);
 
 fun minimize_sort (TSig {classes, ...}) = Sorts.minimize_sort (#2 classes);
 
@@ -622,8 +619,7 @@
 fun add_class context (c, cs) tsig =
   tsig |> map_tsig (fn ((space, classes), default, types) =>
     let
-      val cs' = map (cert_class tsig) cs
-        handle TYPE (msg, _, _) => error msg;
+      val cs' = cert_sort tsig cs handle TYPE (msg, _, _) => error msg;
       val _ = Binding.check c;
       val (c', space') = space |> Name_Space.declare context true c;
       val classes' = classes |> Sorts.add_class context (c', cs');