--- a/src/Pure/General/markup.ML Thu Nov 10 17:47:25 2011 +0100
+++ b/src/Pure/General/markup.ML Thu Nov 10 22:32:10 2011 +0100
@@ -56,6 +56,7 @@
val typN: string val typ: T
val termN: string val term: T
val propN: string val prop: T
+ val typingN: string val typing: T
val ML_keywordN: string val ML_keyword: T
val ML_delimiterN: string val ML_delimiter: T
val ML_tvarN: string val ML_tvar: T
@@ -250,6 +251,8 @@
val (termN, term) = markup_elem "term";
val (propN, prop) = markup_elem "prop";
+val (typingN, typing) = markup_elem "typing";
+
(* ML syntax *)