# HG changeset patch # User wenzelm # Date 1220357427 -7200 # Node ID d6102a4fcfce8d6cd95dec33720699c2809985c4 # Parent b2374a203b1c78671c73914941d24eb881a24bfe added fixed_decl, fact_decl, local_fact_decl; diff -r b2374a203b1c -r d6102a4fcfce src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Tue Sep 02 14:10:25 2008 +0200 +++ b/src/Pure/General/markup.ML Tue Sep 02 14:10:27 2008 +0200 @@ -37,10 +37,13 @@ val fbreakN: string val fbreak: T val tclassN: string val tclass: string -> T val tyconN: string val tycon: string -> T + val fixed_declN: string val fixed_decl: string -> T val fixedN: string val fixed: string -> T val constN: string val const: string -> T + val fact_declN: string val fact_decl: string -> T val factN: string val fact: string -> T val dynamic_factN: string val dynamic_fact: string -> T + val local_fact_declN: string val local_fact_decl: string -> T val local_factN: string val local_fact: string -> T val tfreeN: string val tfree: T val tvarN: string val tvar: T @@ -179,10 +182,13 @@ val (tclassN, tclass) = markup_string "tclass" nameN; val (tyconN, tycon) = markup_string "tycon" nameN; +val (fixed_declN, fixed_decl) = markup_string "fixed_decl" nameN; val (fixedN, fixed) = markup_string "fixed" nameN; val (constN, const) = markup_string "const" nameN; +val (fact_declN, fact_decl) = markup_string "fact_decl" nameN; val (factN, fact) = markup_string "fact" nameN; val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN; +val (local_fact_declN, local_fact_decl) = markup_string "local_fact_decl" nameN; val (local_factN, local_fact) = markup_string "local_fact" nameN;