# HG changeset patch
# User wenzelm
# Date 1321798882 -3600
# Node ID fe57d786fd5bd2befc33ce5712d08b332f4d2b66
# Parent  d320f2f9f331651fd377e2343fcf2effbc0148af
clarified certify vs. sharing;

diff -r d320f2f9f331 -r fe57d786fd5b src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sun Nov 20 13:29:12 2011 +0100
+++ b/src/Pure/sorts.ML	Sun Nov 20 15:21:22 2011 +0100
@@ -38,8 +38,6 @@
   val minimize_sort: algebra -> sort -> sort
   val complete_sort: algebra -> sort -> sort
   val minimal_sorts: algebra -> sort list -> sort Ord_List.T
-  val certify_class: algebra -> class -> class    (*exception TYPE*)
-  val certify_sort: algebra -> sort -> sort       (*exception TYPE*)
   val add_class: Proof.context -> class * class list -> algebra -> algebra
   val add_classrel: Proof.context -> class * class -> algebra -> algebra
   val add_arities: Proof.context -> string * (class * sort list) list -> algebra -> algebra
@@ -182,15 +180,6 @@
   in sorts |> filter_out (fn S => exists (fn S' => le S' S andalso not (le S S')) sorts) end;
 
 
-(* certify *)
-
-fun certify_class algebra c =
-  #1 (Graph.get_entry (classes_of algebra) c)
-    handle Graph.UNDEF _ => raise TYPE ("Undeclared class: " ^ quote c, [], []);
-
-fun certify_sort classes = map (certify_class classes);
-
-
 
 (** build algebras **)
 
diff -r d320f2f9f331 -r fe57d786fd5b src/Pure/term_sharing.ML
--- a/src/Pure/term_sharing.ML	Sun Nov 20 13:29:12 2011 +0100
+++ b/src/Pure/term_sharing.ML	Sun Nov 20 15:21:22 2011 +0100
@@ -21,7 +21,7 @@
   let
     val {classes = (_, algebra), types = (_, types), ...} = Type.rep_tsig (Sign.tsig_of thy);
 
-    val sort = perhaps (try (Sorts.certify_sort algebra));
+    val class = perhaps (try (#1 o Graph.get_entry (Sorts.classes_of algebra)));
     val tycon = perhaps (Option.map #1 o Symtab.lookup_key types);
     val const = perhaps (try (#1 o Consts.the_const (Sign.consts_of thy)));
 
@@ -36,8 +36,8 @@
             val T' =
               (case T of
                 Type (a, Ts) => Type (tycon a, map typ Ts)
-              | TFree (a, S) => TFree (a, sort S)
-              | TVar (a, S) => TVar (a, sort S));
+              | TFree (a, S) => TFree (a, map class S)
+              | TVar (a, S) => TVar (a, map class S));
             val _ = Unsynchronized.change typs (Typtab.update (T', ()));
           in T' end);
 
diff -r d320f2f9f331 -r fe57d786fd5b src/Pure/type.ML
--- a/src/Pure/type.ML	Sun Nov 20 13:29:12 2011 +0100
+++ b/src/Pure/type.ML	Sun Nov 20 15:21:22 2011 +0100
@@ -208,8 +208,12 @@
 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, ...}) = Sorts.certify_class (#2 classes);
-fun cert_sort (TSig {classes, ...}) = Sorts.certify_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 minimize_sort (TSig {classes, ...}) = Sorts.minimize_sort (#2 classes);
 
 fun witness_sorts (TSig {classes, log_types, ...}) =