13 structure ThyParse = ThyParseFun(structure Symtab = Symtab |
13 structure ThyParse = ThyParseFun(structure Symtab = Symtab |
14 and ThyScan = ThyScan); |
14 and ThyScan = ThyScan); |
15 |
15 |
16 use "thy_syn.ML"; |
16 use "thy_syn.ML"; |
17 use "thm_database.ML"; |
17 use "thm_database.ML"; |
|
18 use "../../Provers/simplifier.ML"; |
18 use "thy_read.ML"; |
19 use "thy_read.ML"; |
19 |
20 |
20 structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []); |
21 structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []); |
21 structure ThmDB = ThmDBFun(); |
22 structure ThmDB = ThmDBFUN(); |
22 structure Readthy = ReadthyFUN(structure ThySyn = ThySyn and ThmDB = ThmDB); |
23 structure Simplifier = SimplifierFUN(); |
|
24 structure Readthy = ReadthyFUN(structure ThySyn = ThySyn and ThmDB = ThmDB |
|
25 and Simplifier = Simplifier); |
23 open ThmDB Readthy; |
26 open ThmDB Readthy; |
24 |
27 |
25 (* hide functors; saves space in PolyML *) |
28 (* hide functors; saves space in PolyML *) |
26 functor ThyScanFun() = struct end; |
29 functor ThyScanFun() = struct end; |
27 functor ThyParseFun() = struct end; |
30 functor ThyParseFun() = struct end; |
28 |
31 |
29 fun init_thy_reader () = |
32 fun init_thy_reader () = |
30 use_string |
33 use_string |
31 ["structure ThmDB = ThmDBFun();", |
34 ["structure ThmDB = ThmDBFUN();", |
|
35 "structure Simplifier = SimplifierFUN();", |
32 "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \ |
36 "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \ |
33 \and ThmDB = ThmDB);", |
37 \and ThmDB = ThmDB \ |
|
38 \and Simplifier = Simplifier);", |
34 "Readthy.loaded_thys := !loaded_thys;", |
39 "Readthy.loaded_thys := !loaded_thys;", |
35 "ThmDB.thm_db := !thm_db;", |
40 "ThmDB.thm_db := !thm_db;", |
36 "val first_init_readthy = false;", |
41 "val first_init_readthy = false;", |
37 "open Readthy ThmDB;"]; |
42 "open Readthy ThmDB;"]; |