Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ML_prf: inherit env for all contexts within the proof;
authorwenzelm
Wed, 17 Sep 2008 22:06:54 +0200
changeset 28277 f2995a28e0e4
parent 28276 fbc707811203
child 28278 7af26c1f02ec
ML_prf: inherit env for all contexts within the proof;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_syn.ML	Wed Sep 17 22:06:52 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Sep 17 22:06:54 2008 +0200
@@ -306,7 +306,8 @@
   OuterSyntax.command "ML_prf" "eval ML text within proof" (K.tag_proof K.prf_decl)
     (P.ML_source >> (fn (txt, pos) =>
       Toplevel.proof (Proof.map_context (Context.proof_map
-        (ML_Context.exec (fn () => ML_Context.eval true pos txt))))));
+        (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #>
+          (fn prf => Proof.map_contexts (ML_Context.inherit_env (Proof.context_of prf)) prf))));
 
 val _ =
   OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag)
isabelle