# HG changeset patch
# User wenzelm
# Date 936472032 -7200
# Node ID c7caea1ce78c6e7d21d9ee72cddf88706b5a966a
# Parent  85c8be727fdb4de35cb56f267b1ec1e892ad3cf6
removed text vars;

diff -r 85c8be727fdb -r c7caea1ce78c src/Pure/Isar/outer_lex.ML
--- 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 ||
diff -r 85c8be727fdb -r c7caea1ce78c src/Pure/Isar/outer_parse.ML
--- 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 ||