merged;

--- a/src/Pure/Isar/proof_context.ML	Tue Aug 09 19:26:17 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Aug 09 19:45:01 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 19:26:17 2016 +0200
+++ b/src/Pure/Isar/token.ML	Tue Aug 09 19:45:01 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 =

--- a/src/Pure/ROOT.ML	Tue Aug 09 19:26:17 2016 +0200
+++ b/src/Pure/ROOT.ML	Tue Aug 09 19:45:01 2016 +0200
@@ -186,6 +186,12 @@
 ML_file "skip_proof.ML";
 ML_file "goal.ML";
 
+(*outer syntax*)
+ML_file "Isar/keyword.ML";
+ML_file "Isar/token.ML";
+ML_file "Isar/parse.ML";
+ML_file "Thy/thy_header.ML";
+
 (*proof context*)
 ML_file "Isar/object_logic.ML";
 ML_file "Isar/rule_cases.ML";
@@ -195,18 +201,12 @@
 ML_file "Isar/proof_context.ML";
 ML_file "type_infer_context.ML";
 ML_file "Syntax/syntax_phases.ML";
-ML_file "Isar/local_defs.ML";
-
-(*outer syntax*)
-ML_file "Isar/keyword.ML";
-ML_file "Isar/token.ML";
-ML_file "Isar/parse.ML";
 ML_file "Isar/args.ML";
 
 (*theory specifications*)
+ML_file "Isar/local_defs.ML";
 ML_file "Isar/local_theory.ML";
 ML_file "Isar/entity.ML";
-ML_file "Thy/thy_header.ML";
 ML_file "PIDE/command_span.ML";
 ML_file "Thy/thy_syntax.ML";
 ML_file "Thy/markdown.ML";