diff -r 7bfbd0e07a40 -r e44f1e4fa1f4 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Mon Jun 01 23:28:04 2009 +0200
+++ b/src/Pure/ML/ml_env.ML	Mon Jun 01 23:28:04 2009 +0200
@@ -9,7 +9,7 @@
   val inherit: Context.generic -> Context.generic -> Context.generic
   val register_tokens: ML_Lex.token list -> Context.generic ->
     (serial * ML_Lex.token) list * Context.generic
-  val token_position: Proof.context -> serial -> Position.T option
+  val token_position: Context.generic -> serial -> Position.T option
   val name_space: ML_Name_Space.T
   val local_context: use_context
 end
@@ -57,7 +57,7 @@
       |> Env.map (apfst (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs));
   in (regs, context') end;
 
-val token_position = Inttab.lookup o #1 o Env.get o Context.Proof;
+val token_position = Inttab.lookup o #1 o Env.get;
 
 
 (* results *)