src/Pure/ProofGeneral/parsing.ML

        to reconstruct the input. *)
     (* TODO: see if duplicating isar_output/parse_thy can help here *)
 
     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")
 in
     fun pgip_parser str =