src/Pure/General/markup.ML
changeset 43249 d9fe47d21b41
parent 43248 c113db12bf8b
child 43251 9371ea9f91fb
     1.1 --- a/src/Pure/General/markup.ML	Sun Apr 17 20:25:10 2011 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Sun Apr 17 20:58:43 2011 +0200
     1.3 @@ -39,9 +39,7 @@
     1.4    val fixed_declN: string val fixed_decl: string -> T
     1.5    val fixedN: string val fixed: string -> T
     1.6    val constN: string val const: string -> T
     1.7 -  val factN: string val fact: string -> T
     1.8    val dynamic_factN: string val dynamic_fact: string -> T
     1.9 -  val local_factN: string val local_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 @@ -216,9 +214,7 @@
    1.14  val (fixed_declN, fixed_decl) = markup_string "fixed_decl" nameN;
    1.15  val (fixedN, fixed) = markup_string "fixed" nameN;
    1.16  val (constN, const) = markup_string "constant" nameN;
    1.17 -val (factN, fact) = markup_string "fact" nameN;
    1.18  val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
    1.19 -val (local_factN, local_fact) = markup_string "local_fact" nameN;
    1.20  
    1.21  
    1.22  (* inner syntax *)