# HG changeset patch
# User wenzelm
# Date 1221679651 -7200
# Node ID b1e5e6c4c10e575e1ecf4493210fad90c1338f19
# Parent  ac8431ecd57e98002995c247e64a79c3659fe0b3
added ML_prf;

diff -r ac8431ecd57e -r b1e5e6c4c10e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Sep 17 21:27:24 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Sep 17 21:27:31 2008 +0200
@@ -298,11 +298,17 @@
     (P.path >> (Toplevel.generic_theory o ThyInfo.exec_file false));
 
 val _ =
-  OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.thy_decl)
+  OuterSyntax.command "ML" "eval ML text within theory" (K.tag_ml K.thy_decl)
     (P.ML_source >> (fn (txt, pos) =>
       Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
 
 val _ =
+  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))))));
+
+val _ =
   OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag)
     (P.ML_source >> IsarCmd.ml_diag true);