# HG changeset patch
# User wenzelm
# Date 1620913930 -7200
# Node ID 9267a04aabe6aaffbe8a61b8c4aa8355026d6dc0
# Parent  caa5a257d3edf6db943bfe1e2f3ded56c06e3dd5
tuned;

diff -r caa5a257d3ed -r 9267a04aabe6 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu May 13 15:38:52 2021 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu May 13 15:52:10 2021 +0200
@@ -1532,15 +1532,13 @@
 
 fun print_cases_proof ctxt0 ctxt =
   let
-    val print_name = Token.print_name (Thy_Header.get_keywords' ctxt);
-
     fun trim_name x = if Name.is_internal x then Name.clean x else "_";
     val trim_names = map trim_name #> drop_suffix (equal "_");
 
     fun print_case name xs =
       (case trim_names xs of
-        [] => print_name name
-      | xs' => enclose "(" ")" (space_implode " " (map print_name (name :: xs'))));
+        [] => print_name ctxt name
+      | xs' => enclose "(" ")" (space_implode " " (map (print_name ctxt) (name :: xs'))));
 
     fun is_case x t =
       x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t);