--- a/doc-src/antiquote_setup.ML Wed Sep 17 21:27:36 2008 +0200
+++ b/doc-src/antiquote_setup.ML Wed Sep 17 21:27:38 2008 +0200
@@ -75,7 +75,7 @@
else txt1 ^ ": " ^ txt2;
val txt' = if kind = "" then txt else kind ^ " " ^ txt;
val _ = writeln (ml (txt1, txt2));
- val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2));
+ val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
in
"\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
((if ! O.source then str_of_source src else txt')
--- a/src/Pure/Isar/isar_cmd.ML Wed Sep 17 21:27:36 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Wed Sep 17 21:27:38 2008 +0200
@@ -303,7 +303,8 @@
(* diagnostic ML evaluation *)
fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state =>
- (ML_Context.eval_in (try Toplevel.generic_theory_of state) verbose pos txt));
+ (ML_Context.eval_in
+ (Option.map Context.proof_of (try Toplevel.generic_theory_of state)) verbose pos txt));
(* current working directory *)
--- a/src/Pure/Thy/thy_output.ML Wed Sep 17 21:27:36 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML Wed Sep 17 21:27:38 2008 +0200
@@ -507,7 +507,7 @@
fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
fun output_ml ml src ctxt (txt, pos) =
- (ML_Context.eval_in (SOME (Context.Proof ctxt)) false pos (ml txt);
+ (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
(if ! source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
|> (if ! quotes then quote else I)
|> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"