replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
authorwenzelm
Sun Apr 25 21:18:04 2010 +0200 (2010-04-25)
changeset 363284d9deabf6474
parent 36327 c0415cb24a10
child 36329 85004134055c
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
src/Pure/Isar/class_target.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/axclass.ML
src/Pure/display.ML
src/Pure/sorts.ML
     1.1 --- a/src/Pure/Isar/class_target.ML	Sun Apr 25 21:02:36 2010 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Sun Apr 25 21:18:04 2010 +0200
     1.3 @@ -163,7 +163,7 @@
     1.4        Symtab.empty
     1.5        |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
     1.6             Symtab.map_default (class, []) (insert (op =) tyco)) arities)
     1.7 -             ((#arities o Sorts.rep_algebra) algebra);
     1.8 +             (Sorts.arities_of algebra);
     1.9      val the_arities = these o Symtab.lookup arities;
    1.10      fun mk_arity class tyco =
    1.11        let
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Apr 25 21:02:36 2010 +0200
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Apr 25 21:18:04 2010 +0200
     2.3 @@ -393,7 +393,7 @@
     2.4    let
     2.5      val thy = Toplevel.theory_of state;
     2.6      val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
     2.7 -    val {classes, ...} = Sorts.rep_algebra algebra;
     2.8 +    val classes = Sorts.classes_of algebra;
     2.9      fun entry (c, (i, (_, cs))) =
    2.10        (i, {name = Name_Space.extern space c, ID = c, parents = cs,
    2.11              dir = "", unfold = true, path = ""});
     3.1 --- a/src/Pure/axclass.ML	Sun Apr 25 21:02:36 2010 +0200
     3.2 +++ b/src/Pure/axclass.ML	Sun Apr 25 21:18:04 2010 +0200
     3.3 @@ -176,7 +176,7 @@
     3.4      val certT = Thm.ctyp_of thy;
     3.5  
     3.6      val classrels = fst (get_instances thy);
     3.7 -    val classes = #classes (Sorts.rep_algebra (Sign.classes_of thy));
     3.8 +    val classes = Sorts.classes_of (Sign.classes_of thy);
     3.9  
    3.10      fun reflcl_classrel (c1', c2') =
    3.11        if c1' = c2'
     4.1 --- a/src/Pure/display.ML	Sun Apr 25 21:02:36 2010 +0200
     4.2 +++ b/src/Pure/display.ML	Sun Apr 25 21:18:04 2010 +0200
     4.3 @@ -182,7 +182,8 @@
     4.4      val extern_const = Name_Space.extern (#1 constants);
     4.5      val {classes, default, types, ...} = Type.rep_tsig tsig;
     4.6      val (class_space, class_algebra) = classes;
     4.7 -    val {classes, arities} = Sorts.rep_algebra class_algebra;
     4.8 +    val classes = Sorts.classes_of class_algebra;
     4.9 +    val arities = Sorts.arities_of class_algebra;
    4.10  
    4.11      val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes));
    4.12      val tdecls = Name_Space.dest_table types;
     5.1 --- a/src/Pure/sorts.ML	Sun Apr 25 21:02:36 2010 +0200
     5.2 +++ b/src/Pure/sorts.ML	Sun Apr 25 21:18:04 2010 +0200
     5.3 @@ -25,9 +25,8 @@
     5.4    val insert_term: term -> sort OrdList.T -> sort OrdList.T
     5.5    val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
     5.6    type algebra
     5.7 -  val rep_algebra: algebra ->
     5.8 -   {classes: serial Graph.T,
     5.9 -    arities: (class * (class * sort list)) list Symtab.table}
    5.10 +  val classes_of: algebra -> serial Graph.T
    5.11 +  val arities_of: algebra -> (class * (class * sort list)) list Symtab.table
    5.12    val all_classes: algebra -> class list
    5.13    val super_classes: algebra -> class -> class list
    5.14    val class_less: algebra -> class * class -> bool
    5.15 @@ -116,10 +115,8 @@
    5.16   {classes: serial Graph.T,
    5.17    arities: (class * (class * sort list)) list Symtab.table};
    5.18  
    5.19 -fun rep_algebra (Algebra args) = args;
    5.20 -
    5.21 -val classes_of = #classes o rep_algebra;
    5.22 -val arities_of = #arities o rep_algebra;
    5.23 +fun classes_of (Algebra {classes, ...}) = classes;
    5.24 +fun arities_of (Algebra {arities, ...}) = arities;
    5.25  
    5.26  fun make_algebra (classes, arities) =
    5.27    Algebra {classes = classes, arities = arities};