src/Pure/ML/ml_final.ML

option ML_system_unsafe;

(*  Title:      Pure/ML/ml_final.ML
    Author:     Makarius

Final setup of ML environment.
*)

if Options.default_bool "ML_system_unsafe" then ()
else
  (List.app ML_Name_Space.forget_structure
    ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
   ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);

structure Output: OUTPUT = Output;  (*seal system channels!*)

structure Pure = struct val thy = Thy_Info.pure_theory () end;

Proofterm.proofs := 0;

Context.set_thread_data NONE;