# HG changeset patch
# User wenzelm
# Date 1272223084 -7200
# Node ID 4d9deabf647466d0952558d5f679667d2b5b8a46
# Parent  c0415cb24a105c072f9cdb99a8e702572325849d
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;

diff -r c0415cb24a10 -r 4d9deabf6474 src/Pure/Isar/class_target.ML
--- 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
diff -r c0415cb24a10 -r 4d9deabf6474 src/Pure/Isar/isar_cmd.ML
--- 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 = ""});
diff -r c0415cb24a10 -r 4d9deabf6474 src/Pure/axclass.ML
--- 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'
diff -r c0415cb24a10 -r 4d9deabf6474 src/Pure/display.ML
--- 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;
diff -r c0415cb24a10 -r 4d9deabf6474 src/Pure/sorts.ML
--- 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};