src/Pure/Isar/class.ML
changeset 39133 70d3915c92f0
parent 38757 2b3e054ae6fc
child 39134 917b4b6ba3d2
     1.1 --- a/src/Pure/Isar/class.ML	Sat Sep 04 22:36:42 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sun Sep 05 19:47:40 2010 +0200
     1.3 @@ -525,9 +525,8 @@
     1.4      val params = map_product get_param tycos class_params |> map_filter I;
     1.5      val primary_constraints = map (apsnd
     1.6        (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
     1.7 -    val pp = Syntax.pp_global thy;
     1.8      val algebra = Sign.classes_of thy
     1.9 -      |> fold (fn tyco => Sorts.add_arities pp
    1.10 +      |> fold (fn tyco => Sorts.add_arities (Syntax.pp_global thy)
    1.11              (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
    1.12      val consts = Sign.consts_of thy;
    1.13      val improve_constraints = AList.lookup (op =)