src/Pure/ML/ml_compiler.ML
changeset 62668 360d3464919c
parent 62663 bea354f6ff21
child 62800 7ac100f86863
equal deleted inserted replaced
62667:254582abf067 62668:360d3464919c
   142 
   142 
   143 (* eval ML source tokens *)
   143 (* eval ML source tokens *)
   144 
   144 
   145 fun eval (flags: flags) pos toks =
   145 fun eval (flags: flags) pos toks =
   146   let
   146   let
   147     val _ = Secure.deny_ml ();
       
   148     val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags};
   147     val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags};
   149     val opt_context = Context.thread_data ();
   148     val opt_context = Context.thread_data ();
   150 
   149 
   151 
   150 
   152     (* input *)
   151     (* input *)