src/Pure/Isar/class.ML
changeset 26939 1035c89b4c02
parent 26761 190da765a628
child 26995 2511a72dd73c
     1.1 --- a/src/Pure/Isar/class.ML	Sat May 17 23:53:20 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sun May 18 15:04:09 2008 +0200
     1.3 @@ -722,7 +722,7 @@
     1.4      val inst_params = map_product get_param tycos params |> map_filter I;
     1.5      val primary_constraints = map (apsnd
     1.6        (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) params;
     1.7 -    val pp = Sign.pp thy;
     1.8 +    val pp = Syntax.pp_global thy;
     1.9      val algebra = Sign.classes_of thy
    1.10        |> fold (fn tyco => Sorts.add_arities pp
    1.11              (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
    1.12 @@ -793,7 +793,7 @@
    1.13      fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
    1.14      fun pr_param ((c, _), (v, ty)) =
    1.15        (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
    1.16 -        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Sign.pretty_typ thy ty];
    1.17 +        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty];
    1.18    in
    1.19      (Pretty.block o Pretty.fbreaks)
    1.20        (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)