replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
--- a/src/Pure/Isar/class_target.ML Sun Apr 25 21:02:36 2010 +0200
+++ b/src/Pure/Isar/class_target.ML Sun Apr 25 21:18:04 2010 +0200
@@ -163,7 +163,7 @@
Symtab.empty
|> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
Symtab.map_default (class, []) (insert (op =) tyco)) arities)
- ((#arities o Sorts.rep_algebra) algebra);
+ (Sorts.arities_of algebra);
val the_arities = these o Symtab.lookup arities;
fun mk_arity class tyco =
let
--- a/src/Pure/Isar/isar_cmd.ML Sun Apr 25 21:02:36 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sun Apr 25 21:18:04 2010 +0200
@@ -393,7 +393,7 @@
let
val thy = Toplevel.theory_of state;
val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
- val {classes, ...} = Sorts.rep_algebra algebra;
+ val classes = Sorts.classes_of algebra;
fun entry (c, (i, (_, cs))) =
(i, {name = Name_Space.extern space c, ID = c, parents = cs,
dir = "", unfold = true, path = ""});
--- a/src/Pure/axclass.ML Sun Apr 25 21:02:36 2010 +0200
+++ b/src/Pure/axclass.ML Sun Apr 25 21:18:04 2010 +0200
@@ -176,7 +176,7 @@
val certT = Thm.ctyp_of thy;
val classrels = fst (get_instances thy);
- val classes = #classes (Sorts.rep_algebra (Sign.classes_of thy));
+ val classes = Sorts.classes_of (Sign.classes_of thy);
fun reflcl_classrel (c1', c2') =
if c1' = c2'
--- a/src/Pure/display.ML Sun Apr 25 21:02:36 2010 +0200
+++ b/src/Pure/display.ML Sun Apr 25 21:18:04 2010 +0200
@@ -182,7 +182,8 @@
val extern_const = Name_Space.extern (#1 constants);
val {classes, default, types, ...} = Type.rep_tsig tsig;
val (class_space, class_algebra) = classes;
- val {classes, arities} = Sorts.rep_algebra class_algebra;
+ val classes = Sorts.classes_of class_algebra;
+ val arities = Sorts.arities_of class_algebra;
val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes));
val tdecls = Name_Space.dest_table types;
--- a/src/Pure/sorts.ML Sun Apr 25 21:02:36 2010 +0200
+++ b/src/Pure/sorts.ML Sun Apr 25 21:18:04 2010 +0200
@@ -25,9 +25,8 @@
val insert_term: term -> sort OrdList.T -> sort OrdList.T
val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
type algebra
- val rep_algebra: algebra ->
- {classes: serial Graph.T,
- arities: (class * (class * sort list)) list Symtab.table}
+ val classes_of: algebra -> serial Graph.T
+ val arities_of: algebra -> (class * (class * sort list)) list Symtab.table
val all_classes: algebra -> class list
val super_classes: algebra -> class -> class list
val class_less: algebra -> class * class -> bool
@@ -116,10 +115,8 @@
{classes: serial Graph.T,
arities: (class * (class * sort list)) list Symtab.table};
-fun rep_algebra (Algebra args) = args;
-
-val classes_of = #classes o rep_algebra;
-val arities_of = #arities o rep_algebra;
+fun classes_of (Algebra {classes, ...}) = classes;
+fun arities_of (Algebra {arities, ...}) = arities;
fun make_algebra (classes, arities) =
Algebra {classes = classes, arities = arities};