equal
deleted
inserted
replaced
13 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
13 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
14 |
14 |
15 SML_import \<open> |
15 SML_import \<open> |
16 structure Output_Primitives = Output_Primitives_Virtual; |
16 structure Output_Primitives = Output_Primitives_Virtual; |
17 structure Thread_Data = Thread_Data_Virtual; |
17 structure Thread_Data = Thread_Data_Virtual; |
|
18 fun ML_system_pp (_: int -> 'a -> 'b -> PolyML_Pretty.pretty) = (); |
18 \<close> |
19 \<close> |
19 |
20 |
20 |
21 |
21 subsection \<open>Final setup of global ML environment\<close> |
22 subsection \<open>Final setup of global ML environment\<close> |
22 |
23 |