src/Pure/Isar/parse.ML

   val params: (binding * string option) list parser
   val simple_fixes: (binding * string option) list parser
   val fixes: (binding * string option * mixfix) list parser
   val for_fixes: (binding * string option * mixfix) list parser
   val ML_source: (Symbol_Pos.text * Position.T) parser
-  val doc_source: (Symbol_Pos.text * Position.T) parser
+  val document_source: (Symbol_Pos.text * Position.T) parser
   val term_group: string parser
   val prop_group: string parser
   val term: string parser
   val prop: string parser
   val const: string parser

 
 
 (* embedded source text *)
 
 val ML_source = source_position (group (fn () => "ML source") text);
-val doc_source = source_position (group (fn () => "document source") text);
+val document_source = source_position (group (fn () => "document source") text);
 
 
 (* terms *)
 
 val tm = short_ident || long_ident || sym_ident || term_var || number || string;