src/Pure/Isar/parse.ML
changeset 51627 589daaf48dba
parent 48927 ef462b5558eb
child 51654 8450b944e58a
--- a/src/Pure/Isar/parse.ML	Fri Apr 05 20:43:43 2013 +0200
+++ b/src/Pure/Isar/parse.ML	Fri Apr 05 20:54:55 2013 +0200
@@ -91,7 +91,7 @@
   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
@@ -341,7 +341,7 @@
 (* 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 *)