src/Pure/Thy/ROOT.ML
changeset 1512 ce37c64244c0
parent 1457 ad856378ad62
child 2404 edcc26b1461d
     1.1 --- a/src/Pure/Thy/ROOT.ML	Fri Feb 16 17:24:51 1996 +0100
     1.2 +++ b/src/Pure/Thy/ROOT.ML	Fri Feb 16 18:00:47 1996 +0100
     1.3 @@ -8,17 +8,10 @@
     1.4  
     1.5  use "thy_scan.ML";
     1.6  use "thy_parse.ML";
     1.7 -
     1.8 -structure ThyScan = ThyScanFun(Scanner);
     1.9 -structure ThyParse = ThyParseFun(structure Symtab = Symtab
    1.10 -  and ThyScan = ThyScan);
    1.11 -
    1.12  use "thy_syn.ML";
    1.13  use "thm_database.ML";
    1.14  use "../../Provers/simplifier.ML";
    1.15  
    1.16 -structure Simplifier = SimplifierFun();
    1.17 -
    1.18  use "thy_read.ML";
    1.19  
    1.20  structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
    1.21 @@ -26,10 +19,6 @@
    1.22  structure ReadThy = ReadthyFun(structure ThySyn = ThySyn and ThmDB = ThmDB);
    1.23  open ThmDB ReadThy;
    1.24  
    1.25 -(* hide functors; saves space in PolyML *)
    1.26 -functor ThyScanFun() = struct end;
    1.27 -functor ThyParseFun() = struct end;
    1.28 -functor SimplifierFun() = struct end;
    1.29  
    1.30  fun init_thy_reader () =
    1.31    use_string