equal
deleted
inserted
replaced
6 |
6 |
7 theory ML_Bootstrap |
7 theory ML_Bootstrap |
8 imports Pure |
8 imports Pure |
9 begin |
9 begin |
10 |
10 |
|
11 subsection \<open>Standard ML environment for virtual bootstrap\<close> |
|
12 |
11 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
13 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
12 |
14 |
13 SML_import \<open> |
15 SML_import \<open> |
14 structure Output_Primitives = Output_Primitives_Virtual; |
16 structure Output_Primitives = Output_Primitives_Virtual; |
15 structure Thread_Data = Thread_Data_Virtual; |
17 structure Thread_Data = Thread_Data_Virtual; |
16 \<close> |
18 \<close> |
|
19 |
|
20 |
|
21 subsection \<open>Final setup of global ML environment\<close> |
|
22 |
|
23 ML \<open>Proofterm.proofs := 0\<close> |
|
24 |
|
25 ML \<open> |
|
26 Context.setmp_generic_context NONE |
|
27 ML \<open> |
|
28 List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures; |
|
29 structure PolyML = struct structure IntInf = PolyML.IntInf end; |
|
30 \<close> |
|
31 \<close> |
|
32 |
|
33 ML \<open>@{assert} (not (can ML \<open>open RunCall\<close>))\<close> |
|
34 |
|
35 |
|
36 subsection \<open>Switch to bootstrap environment\<close> |
17 |
37 |
18 setup \<open>Config.put_global ML_Env.SML_environment true\<close> |
38 setup \<open>Config.put_global ML_Env.SML_environment true\<close> |
19 |
39 |
20 end |
40 end |