added fixedN, constN;
authorwenzelm
Fri, 10 Feb 2006 02:22:50 +0100
changeset 19002 2fbb3d809026
parent 19001 64e4b5bc6443
child 19003 64ad6c520464
added fixedN, constN;
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 *)