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