equal
deleted
inserted
replaced
10 |
10 |
11 structure Output: OUTPUT = Output; (*seal system channels!*) |
11 structure Output: OUTPUT = Output; (*seal system channels!*) |
12 |
12 |
13 structure Pure = struct val thy = Thy_Info.pure_theory () end; |
13 structure Pure = struct val thy = Thy_Info.pure_theory () end; |
14 |
14 |
15 fun use_thys args = |
|
16 Runtime.toplevel_program (fn () => Thy_Info.use_thys (map (rpair Position.none) args)); |
|
17 val use_thy = use_thys o single; |
|
18 |
|
19 Proofterm.proofs := 0; |
15 Proofterm.proofs := 0; |
20 |
16 |
21 Context.set_thread_data NONE; |
17 Context.set_thread_data NONE; |