src/Pure/Isar/element.ML

   let
     val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     val prt_terms = separate (Pretty.keyword2 "and") o map prt_term;
     val prt_binding = Attrib.pretty_binding ctxt;
+    val prt_name = Proof_Context.pretty_name ctxt;
 
     fun prt_show (a, ts) =
       Pretty.block (Pretty.breaks (prt_binding a ":" @ prt_terms (map fst ts)));
 
     fun prt_var (x, SOME T, _) = Pretty.block
-          [Pretty.str (Binding.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
-      | prt_var (x, NONE, _) = Pretty.str (Binding.name_of x);
+          [prt_name (Binding.name_of x), Pretty.str " ::", Pretty.brk 1, prt_typ T]
+      | prt_var (x, NONE, _) = prt_name (Binding.name_of x);
     val prt_vars = separate (Pretty.keyword2 "and") o map prt_var;
 
     fun prt_obtain (_, ([], props)) = Pretty.block (Pretty.breaks (prt_terms props))
       | prt_obtain (_, (vars, props)) = Pretty.block (Pretty.breaks
           (prt_vars vars @ [Pretty.keyword2 "where"] @ prt_terms props));

 fun gen_pretty_ctxt show_attribs ctxt =
   let
     val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
+    val prt_name = Proof_Context.pretty_name ctxt;
 
     fun prt_binding (b, atts) =
       Attrib.pretty_binding ctxt (b, if show_attribs then atts else []);
 
     fun prt_fact (ths, atts) =

           Attrib.pretty_attribs ctxt atts;
 
     fun prt_mixfix NoSyn = []
       | prt_mixfix mx = [Pretty.brk 2, Mixfix.pretty_mixfix mx];
 
-    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.name_of x ^ " ::") ::
+    fun prt_fix (x, SOME T, mx) = Pretty.block (prt_name (Binding.name_of x) :: Pretty.str " ::" ::
           Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
-      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.name_of x) ::
+      | prt_fix (x, NONE, mx) = Pretty.block (prt_name (Binding.name_of x) ::
           Pretty.brk 1 :: prt_mixfix mx);
     fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
 
     fun prt_asm (a, ts) =
       Pretty.block (Pretty.breaks (prt_binding a ":" @ map (prt_term o fst) ts));

         val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
         val th' = Thm.instantiate ([], [(Term.dest_Var C, Thm.cterm_of ctxt thesis)]) th;
       in (th', true) end
   | NONE => (th, false));
 
-fun thm_name kind th prts =
+fun thm_name ctxt kind th prts =
   let val head =
     if Thm.has_name_hint th then
-      Pretty.block [Pretty.keyword1 kind,
-        Pretty.brk 1, Pretty.str (Long_Name.base_name (Thm.get_name_hint th) ^ ":")]
+      Pretty.block [Pretty.keyword1 kind, Pretty.brk 1,
+        Proof_Context.pretty_name ctxt (Long_Name.base_name (Thm.get_name_hint th)), Pretty.str ":"]
     else Pretty.keyword1 kind
   in Pretty.block (Pretty.fbreaks (head :: prts)) end;
 
 fun obtain prop ctxt =
   let

     pretty_ctxt ctxt' (Assumes (map (fn t => (Binding.empty_atts, [(t, [])])) assumes)) @
      (if null cases then pretty_stmt ctxt' (Shows [(Binding.empty_atts, [(concl, [])])])
       else
         let val (clauses, ctxt'') = fold_map obtain cases ctxt'
         in pretty_stmt ctxt'' (Obtains clauses) end)
-  end |> thm_name kind raw_th;
+  end |> thm_name ctxt kind raw_th;
 
 end;