1.1 --- a/doc-src/antiquote_setup.ML	Wed Sep 17 21:27:36 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Wed Sep 17 21:27:38 2008 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4        else txt1 ^ ": " ^ txt2;
     1.5      val txt' = if kind = "" then txt else kind ^ " " ^ txt;
     1.6      val _ = writeln (ml (txt1, txt2));
     1.7 -    val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2));
     1.8 +    val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
     1.9    in
    1.10      "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
    1.11      ((if ! O.source then str_of_source src else txt')

     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Sep 17 21:27:36 2008 +0200
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Sep 17 21:27:38 2008 +0200
     2.3 @@ -303,7 +303,8 @@
     2.4  (* diagnostic ML evaluation *)
     2.5  
     2.6  fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state =>
     2.7 -  (ML_Context.eval_in (try Toplevel.generic_theory_of state) verbose pos txt));
     2.8 +  (ML_Context.eval_in
     2.9 +    (Option.map Context.proof_of (try Toplevel.generic_theory_of state)) verbose pos txt));
    2.10  
    2.11  
    2.12  (* current working directory *)

     3.1 --- a/src/Pure/Thy/thy_output.ML	Wed Sep 17 21:27:36 2008 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Sep 17 21:27:38 2008 +0200
     3.3 @@ -507,7 +507,7 @@
     3.4  fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
     3.5  
     3.6  fun output_ml ml src ctxt (txt, pos) =
     3.7 - (ML_Context.eval_in (SOME (Context.Proof ctxt)) false pos (ml txt);
     3.8 + (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
     3.9    (if ! source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
    3.10    |> (if ! quotes then quote else I)
    3.11    |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"