tuned signature;
authorwenzelm
Mon Jun 01 23:28:04 2009 +0200 (2009-06-01)
changeset 31331e44f1e4fa1f4
parent 31330 7bfbd0e07a40
child 31332 9639a6d4d714
tuned signature;
src/Pure/ML/ml_env.ML
     1.1 --- a/src/Pure/ML/ml_env.ML	Mon Jun 01 23:28:04 2009 +0200
     1.2 +++ b/src/Pure/ML/ml_env.ML	Mon Jun 01 23:28:04 2009 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4    val inherit: Context.generic -> Context.generic -> Context.generic
     1.5    val register_tokens: ML_Lex.token list -> Context.generic ->
     1.6      (serial * ML_Lex.token) list * Context.generic
     1.7 -  val token_position: Proof.context -> serial -> Position.T option
     1.8 +  val token_position: Context.generic -> serial -> Position.T option
     1.9    val name_space: ML_Name_Space.T
    1.10    val local_context: use_context
    1.11  end
    1.12 @@ -57,7 +57,7 @@
    1.13        |> Env.map (apfst (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs));
    1.14    in (regs, context') end;
    1.15  
    1.16 -val token_position = Inttab.lookup o #1 o Env.get o Context.Proof;
    1.17 +val token_position = Inttab.lookup o #1 o Env.get;
    1.18  
    1.19  
    1.20  (* results *)