--- a/src/Pure/Isar/isar_syn.ML Sat Mar 01 19:55:01 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Mar 01 22:46:31 2014 +0100
@@ -248,16 +248,17 @@
val _ =
Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
- (Parse.ML_source >> (fn (txt, pos) =>
+ (Parse.ML_source >> (fn source =>
Toplevel.generic_theory
- (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
+ (ML_Context.exec (fn () => ML_Context.eval_source true source) #>
Local_Theory.propagate_ml_env)));
val _ =
Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
- (Parse.ML_source >> (fn (txt, pos) =>
+ (Parse.ML_source >> (fn source =>
Toplevel.proof (Proof.map_context (Context.proof_map
- (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));
+ (ML_Context.exec (fn () => ML_Context.eval_source true source))) #>
+ Proof.propagate_ml_env)));
val _ =
Outer_Syntax.command @{command_spec "ML_val"} "diagnostic ML text"