# HG changeset patch
# User wenzelm
# Date 1237412475 -3600
# Node ID 7e5b9bbc54d86f0a205978a51ff36068e152416c
# Parent  368e26dfba6931543fd754294142cf15ed84f7c8
generalized ML_Context.inherit_env;

diff -r 368e26dfba69 -r 7e5b9bbc54d8 src/Pure/Isar/isar_syn.ML
--- 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)