src/Pure/Isar/class_target.ML
changeset 36328 4d9deabf6474
parent 36323 655e2d74de3a
child 36462 70a1e6accac3
     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