# HG changeset patch
# User wenzelm
# Date 1378906925 -7200
# Node ID 51157ee7f5ba5867cc400083bed47e19644fc818
# Parent  4e9e150422d554611078e623b85b1559cd1c662c
tuned signature;

diff -r 4e9e150422d5 -r 51157ee7f5ba src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Sep 11 15:30:12 2013 +0200
+++ b/src/Pure/General/name_space.ML	Wed Sep 11 15:42:05 2013 +0200
@@ -30,6 +30,7 @@
   val extern: Proof.context -> T -> string -> xstring
   val extern_ord: Proof.context -> T -> string * string -> order
   val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
+  val pretty: Proof.context -> T -> string -> Pretty.T
   val hide: bool -> string -> T -> T
   val merge: T * T -> T
   type naming
@@ -194,6 +195,8 @@
 
 fun markup_extern ctxt space name = (markup space name, extern ctxt space name);
 
+fun pretty ctxt space name = Pretty.mark_str (markup_extern ctxt space name);
+
 
 (* modify internals *)
 
diff -r 4e9e150422d5 -r 51157ee7f5ba src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Sep 11 15:30:12 2013 +0200
+++ b/src/Pure/Isar/class.ML	Wed Sep 11 15:42:05 2013 +0200
@@ -182,14 +182,14 @@
 
     fun prt_param (c, ty) =
       Pretty.block
-       [Pretty.mark_str (Name_Space.markup_extern ctxt const_space c), Pretty.str " ::",
+       [Name_Space.pretty ctxt const_space c, Pretty.str " ::",
         Pretty.brk 1, Syntax.pretty_typ ctxt (Type.strip_sorts_dummy ty)];
 
     fun prt_entry class =
       Pretty.block
         ([Pretty.command "class", Pretty.brk 1,
-          Pretty.mark_str (Name_Space.markup_extern ctxt class_space class), Pretty.str ":",
-          Pretty.fbrk, Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
+          Name_Space.pretty ctxt class_space class, Pretty.str ":", Pretty.fbrk,
+          Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
           (case try (Axclass.get_info thy) class of
             NONE => []
           | SOME {params, ...} =>
diff -r 4e9e150422d5 -r 51157ee7f5ba src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Wed Sep 11 15:30:12 2013 +0200
+++ b/src/Tools/subtyping.ML	Wed Sep 11 15:42:05 2013 +0200
@@ -1046,9 +1046,9 @@
     val tmaps =
       sort (Name_Space.extern_ord ctxt type_space o pairself #1)
         (Symtab.dest (tmaps_of ctxt));
-    fun show_map (x, (t, _)) =
+    fun show_map (c, (t, _)) =
       Pretty.block
-       [Pretty.mark_str (Name_Space.markup_extern ctxt type_space x), Pretty.str ":",
+       [Name_Space.pretty ctxt type_space c, Pretty.str ":",
         Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt t)];
   in
    [Pretty.big_list "coercions between base types:" (map show_coercion simple),