--- a/src/Pure/Isar/outer_lex.ML Sat Sep 04 21:06:20 1999 +0200
+++ b/src/Pure/Isar/outer_lex.ML Sat Sep 04 21:07:12 1999 +0200
@@ -8,7 +8,7 @@
signature OUTER_LEX =
sig
datatype token_kind =
- Command | Keyword | Ident | LongIdent | SymIdent | Var | TextVar | TypeIdent | TypeVar |
+ Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
Nat | String | Verbatim | Ignore | Sync | EOF
type token
val str_of_kind: token_kind -> string
@@ -39,7 +39,7 @@
(* datatype token *)
datatype token_kind =
- Command | Keyword | Ident | LongIdent | SymIdent | Var | TextVar | TypeIdent | TypeVar |
+ Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
Nat | String | Verbatim | Ignore | Sync | EOF;
datatype token = Token of Position.T * (token_kind * string);
@@ -51,7 +51,6 @@
| LongIdent => "long identifier"
| SymIdent => "symbolic identifier"
| Var => "schematic variable"
- | TextVar => "text variable"
| TypeIdent => "type variable"
| TypeVar => "schematic type variable"
| Nat => "number"
@@ -210,7 +209,6 @@
(Syntax.scan_longid >> token LongIdent ||
Syntax.scan_id >> token Ident ||
Syntax.scan_var >> token Var ||
- $$ "?" ^^ $$ "?" ^^ Syntax.scan_id >> token TextVar ||
Syntax.scan_tid >> token TypeIdent ||
Syntax.scan_tvar >> token TypeVar ||
Syntax.scan_nat >> token Nat ||
--- a/src/Pure/Isar/outer_parse.ML Sat Sep 04 21:06:20 1999 +0200
+++ b/src/Pure/Isar/outer_parse.ML Sat Sep 04 21:07:12 1999 +0200
@@ -18,7 +18,6 @@
val long_ident: token list -> string * token list
val sym_ident: token list -> string * token list
val term_var: token list -> string * token list
- val text_var: token list -> string * token list
val type_ident: token list -> string * token list
val type_var: token list -> string * token list
val number: token list -> string * token list
@@ -121,7 +120,6 @@
val long_ident = kind OuterLex.LongIdent;
val sym_ident = kind OuterLex.SymIdent;
val term_var = kind OuterLex.Var;
-val text_var = kind OuterLex.TextVar;
val type_ident = kind OuterLex.TypeIdent;
val type_var = kind OuterLex.TypeVar;
val number = kind OuterLex.Nat;
@@ -222,7 +220,7 @@
(* terms *)
-val trm = short_ident || long_ident || sym_ident || term_var || text_var || number || string;
+val trm = short_ident || long_ident || sym_ident || term_var || number || string;
val term = group "term" trm;
val prop = group "proposition" trm;
@@ -245,7 +243,7 @@
fun atom_arg is_symid blk =
group "argument"
- (position (short_ident || long_ident || sym_ident || term_var || text_var ||
+ (position (short_ident || long_ident || sym_ident || term_var ||
type_ident || type_var || number) >> Args.ident ||
position (keyword_symid is_symid) >> Args.keyword ||
position string >> Args.string ||