clarified certify vs. sharing;
--- 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 **)
--- 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);
--- 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, ...}) =