Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/isar_output.ML
changeset 22086 cf6019fece63
parent 21879 a3efbae45735 
--- a/src/Pure/Isar/isar_output.ML	Fri Jan 19 13:09:32 2007 +0100
+++ b/src/Pure/Isar/isar_output.ML	Fri Jan 19 13:09:33 2007 +0100
@@ -509,7 +509,7 @@
 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
 
 fun output_ml ml src ctxt txt =
- (Context.use_mltext (ml txt) false (SOME (ProofContext.theory_of ctxt));
+ (Context.use_mltext (ml txt) false (SOME (Context.Proof ctxt));
   (if ! source then str_of_source src else txt)
   |> (if ! quotes then quote else I)
   |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
isabelle