equal
deleted
inserted
replaced
7 (* the Pure theories *) |
7 (* the Pure theories *) |
8 |
8 |
9 val theory = ThyInfo.get_theory; |
9 val theory = ThyInfo.get_theory; |
10 |
10 |
11 Context.>> (Context.map_theory |
11 Context.>> (Context.map_theory |
12 (OuterSyntax.process_file (Path.explode "Pure.thy") #> |
12 (Outer_Syntax.process_file (Path.explode "Pure.thy") #> |
13 Theory.end_theory)); |
13 Theory.end_theory)); |
14 structure Pure = struct val thy = ML_Context.the_global_context () end; |
14 structure Pure = struct val thy = ML_Context.the_global_context () end; |
15 Context.set_thread_data NONE; |
15 Context.set_thread_data NONE; |
16 ThyInfo.register_theory Pure.thy; |
16 ThyInfo.register_theory Pure.thy; |
17 |
17 |