# HG changeset patch
# User wenzelm
# Date 1220456857 -7200
# Node ID f6e38928b77cd7ba879db65f86713db696124fd6
# Parent  691993ef6abed63f1b1b52d9967a98a852b8ce40
added const_decl;

diff -r 691993ef6abe -r f6e38928b77c src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Wed Sep 03 17:47:35 2008 +0200
+++ b/src/Pure/General/markup.ML	Wed Sep 03 17:47:37 2008 +0200
@@ -39,6 +39,7 @@
   val tyconN: string val tycon: string -> T
   val fixed_declN: string val fixed_decl: string -> T
   val fixedN: string val fixed: string -> T
+  val const_declN: string val const_decl: 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
@@ -184,6 +185,7 @@
 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 (const_declN, const_decl) = markup_string "const_decl" 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;