# HG changeset patch
# User wenzelm
# Date 1139534570 -3600
# Node ID 2fbb3d809026617f8ffe8a1d7c71d30abcaa9f20
# Parent  64e4b5bc644302b36894c7f1d812ea8638680e28
added fixedN, constN;

diff -r 64e4b5bc6443 -r 2fbb3d809026 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri Feb 10 02:22:48 2006 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Fri Feb 10 02:22:50 2006 +0100
@@ -33,6 +33,8 @@
   val read_nat: string -> int option
   val read_xnum: string -> IntInf.int
   val read_idents: string -> string list
+  val fixedN: string
+  val constN: string
 end;
 
 signature LEXICON =
@@ -348,7 +350,7 @@
   in Scan.read Symbol.stopper scan (Symbol.explode str) end;
 
 
-(* variable kinds *)
+(* specific identifiers *)
 
 val internal = suffix "_";
 val dest_internal = unsuffix "_";
@@ -356,6 +358,9 @@
 val skolem = suffix "__";
 val dest_skolem = unsuffix "__";
 
+val constN = "\\<^const>";
+val fixedN = "\\<^fixed>";
+
 
 (* read_nat *)