1.1 --- a/src/Pure/General/markup.ML	Tue Aug 05 13:31:35 2008 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Tue Aug 05 13:31:36 2008 +0200
     1.3 @@ -37,7 +37,8 @@
     1.4    val tyconN: string val tycon: string -> T
     1.5    val fixedN: string val fixed: string -> T
     1.6    val constN: string val const: string -> T
     1.7 -  val axiomN: string val axiom: string -> T
     1.8 +  val factN: string val fact: string -> T
     1.9 +  val dynamic_factN: string val dynamic_fact: string -> T
    1.10    val tfreeN: string val tfree: T
    1.11    val tvarN: string val tvar: T
    1.12    val freeN: string val free: T
    1.13 @@ -50,6 +51,7 @@
    1.14    val sortN: string val sort: T
    1.15    val typN: string val typ: T
    1.16    val termN: string val term: T
    1.17 +  val propN: string val prop: T
    1.18    val keywordN: string val keyword: string -> T
    1.19    val commandN: string val command: string -> T
    1.20    val keyword_declN: string val keyword_decl: string -> T
    1.21 @@ -150,7 +152,8 @@
    1.22  val (tyconN, tycon) = markup_string "tycon" nameN;
    1.23  val (fixedN, fixed) = markup_string "fixed" nameN;
    1.24  val (constN, const) = markup_string "const" nameN;
    1.25 -val (axiomN, axiom) = markup_string "axiom" nameN;
    1.26 +val (factN, fact) = markup_string "fact" nameN;
    1.27 +val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
    1.28  
    1.29  
    1.30  (* inner syntax *)
    1.31 @@ -168,6 +171,7 @@
    1.32  val (sortN, sort) = markup_elem "sort";
    1.33  val (typN, typ) = markup_elem "typ";
    1.34  val (termN, term) = markup_elem "term";
    1.35 +val (propN, prop) = markup_elem "prop";
    1.36  
    1.37  
    1.38  (* outer syntax *)