print name in parsable form;

--- a/src/Pure/Isar/proof_context.ML	Tue Aug 09 14:41:27 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Aug 09 19:44:28 2016 +0200
@@ -1528,13 +1528,15 @@
 
 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 #> take_suffix (equal "_") #> #1;
 
     fun print_case name xs =
       (case trim_names xs of
-        [] => name
-      | xs' => enclose "(" ")" (space_implode " " (name :: xs')));
+        [] => print_name name
+      | xs' => enclose "(" ")" (space_implode " " (map print_name (name :: xs'))));
 
     fun is_case x t =
       x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t);

--- a/src/Pure/Isar/token.ML	Tue Aug 09 14:41:27 2016 +0200
+++ b/src/Pure/Isar/token.ML	Tue Aug 09 19:44:28 2016 +0200
@@ -91,6 +91,7 @@
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
   val read_cartouche: Symbol_Pos.T list -> T
   val explode: Keyword.keywords -> Position.T -> string -> T list
+  val print_name: Keyword.keywords -> string -> string
   val make: (int * int) * string -> Position.T -> T * Position.T
   val make_string: string * Position.T -> T
   val make_int: int -> T list
@@ -655,6 +656,14 @@
   Source.exhaust;
 
 
+(* print name in parsable form *)
+
+fun print_name keywords name =
+  ((case explode keywords Position.none name of
+    [tok] => not (member (op =) [Ident, Long_Ident, Sym_Ident, Nat] (kind_of tok))
+  | _ => true) ? Symbol_Pos.quote_string_qq) name;
+
+
 (* make *)
 
 fun make ((k, n), s) pos =