--- a/src/Pure/Isar/outer_syntax.ML Mon Apr 04 17:02:34 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Mon Apr 04 17:25:53 2016 +0200
@@ -306,4 +306,15 @@
in error ("Bad command " ^ quote name ^ Position.here pos ^ report) end
end;
+
+(* 'ML' command -- required for bootstrapping Isar *)
+
+val _ =
+ command ("ML", @{here}) "ML text within theory or local theory"
+ (Parse.ML_source >> (fn source =>
+ Toplevel.generic_theory
+ (ML_Context.exec (fn () =>
+ ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
+ Local_Theory.propagate_ml_env)));
+
end;