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.
generalized ML_Context.inherit_env;
authorwenzelm
Wed, 18 Mar 2009 22:41:15 +0100
changeset 30576 7e5b9bbc54d8
parent 30575 368e26dfba69
child 30577 79cc595655c0
generalized ML_Context.inherit_env;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_syn.ML	Wed Mar 18 22:41:14 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 18 22:41:15 2009 +0100
@@ -309,7 +309,8 @@
     (P.ML_source >> (fn (txt, pos) =>
       Toplevel.proof (Proof.map_context (Context.proof_map
         (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #>
-          (fn prf => Proof.map_contexts (ML_Context.inherit_env (Proof.context_of prf)) prf))));
+          (fn prf => prf |> Proof.map_contexts
+            (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf))))))));
 
 val _ =
   OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag)
isabelle