src/Pure/General/markup.ML

   val get_string: T -> string -> string option
   val get_int: T -> string -> int option
   val none: T
   val properties: (string * string) list -> T -> T
   val nameN: string
+  val name: string -> T -> T
   val groupN: string
   val theory_nameN: string
   val idN: string
   val kindN: string
   val internalK: string

   val tyconN: string val tycon: string -> T
   val fixedN: string val fixed: string -> T
   val constN: string val const: string -> T
   val factN: string val fact: string -> T
   val dynamic_factN: string val dynamic_fact: string -> T
+  val local_factN: string val local_fact: string -> T
   val tfreeN: string val tfree: T
   val tvarN: string val tvar: T
   val freeN: string val free: T
   val skolemN: string val skolem: T
   val boundN: string val bound: T

   val xstrN: string val xstr: T
   val literalN: string val literal: T
   val sortN: string val sort: T
   val typN: string val typ: T
   val termN: string val term: T
-  val propositionN: string val proposition: T
+  val propN: string val prop: T
   val attributeN: string val attribute: string -> T
   val methodN: string val method: string -> T
   val keywordN: string val keyword: string -> T
   val commandN: string val command: string -> T
   val keyword_declN: string val keyword_decl: string -> T

 
 
 (* name *)
 
 val nameN = "name";
+fun name a = properties [(nameN, a)];
+
 val groupN = "group";
 val theory_nameN = "theory_name";
 
 
 (* kind *)

 val (tyconN, tycon) = markup_string "tycon" nameN;
 val (fixedN, fixed) = markup_string "fixed" nameN;
 val (constN, const) = markup_string "const" nameN;
 val (factN, fact) = markup_string "fact" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
+val (local_factN, local_fact) = markup_string "local_fact" nameN;
 
 
 (* inner syntax *)
 
 val (tfreeN, tfree) = markup_elem "tfree";

 val (literalN, literal) = markup_elem "literal";
 
 val (sortN, sort) = markup_elem "sort";
 val (typN, typ) = markup_elem "typ";
 val (termN, term) = markup_elem "term";
-val (propositionN, proposition) = markup_elem "proposition";
+val (propN, prop) = markup_elem "prop";
 
 val (attributeN, attribute) = markup_string "attribute" nameN;
 val (methodN, method) = markup_string "method" nameN;