# HG changeset patch
# User wenzelm
# Date 1167491286 -3600
# Node ID edab0ecfbd7cd915fc6f0debd43f7c4123ffc7f6
# Parent  7120ef5bc37870e10387cc9dd6f20e46b106db46
removed misleading OuterLex.eq_token;

diff -r 7120ef5bc378 -r edab0ecfbd7c src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Sat Dec 30 16:08:05 2006 +0100
+++ b/src/Pure/Isar/outer_lex.ML	Sat Dec 30 16:08:06 2006 +0100
@@ -11,7 +11,6 @@
     Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
     Nat | String | AltString | Verbatim | Space | Comment | Sync | Malformed | EOF
   eqtype token
-  val eq_token: token * token -> bool
   val str_of_kind: token_kind -> string
   val stopper: token * (token -> bool)
   val not_sync: token -> bool
@@ -62,8 +61,6 @@
 
 datatype token = Token of Position.T * (token_kind * string);
 
-val eq_token = op = : token * token -> bool;
-
 val str_of_kind =
  fn Command => "command"
   | Keyword => "keyword"
diff -r 7120ef5bc378 -r edab0ecfbd7c src/Pure/ProofGeneral/parsing.ML
--- a/src/Pure/ProofGeneral/parsing.ML	Sat Dec 30 16:08:05 2006 +0100
+++ b/src/Pure/ProofGeneral/parsing.ML	Sat Dec 30 16:08:06 2006 +0100
@@ -300,7 +300,7 @@
 
     fun match_tokens ([],us,vs) = (rev vs,us)  (* used, unused *)
       | match_tokens (t::ts, w::ws, vs) =
-        if OuterLex.eq_token (t, w)
+        if (t: OuterLex.token) = w  (* FIXME !? *)
           then match_tokens (ts, ws, w::vs)
           else match_tokens (t::ts, ws, w::vs)
       | match_tokens _ = error ("match_tokens: mismatched input parse")