# HG changeset patch # User clasohm # Date 812807870 -3600 # Node ID af4107a031500e1a445b532d3f8415f49491e6f3 # Parent c76ac4a9dc2b1077ee47fe38d2e700804ae7591c changed usage of structure Simplifier diff -r c76ac4a9dc2b -r af4107a03150 src/Pure/Thy/ROOT.ML --- a/src/Pure/Thy/ROOT.ML Wed Oct 04 12:53:35 1995 +0100 +++ b/src/Pure/Thy/ROOT.ML Wed Oct 04 12:57:50 1995 +0100 @@ -16,27 +16,26 @@ use "thy_syn.ML"; use "thm_database.ML"; use "../../Provers/simplifier.ML"; + +structure Simplifier = SimplifierFun(); + use "thy_read.ML"; structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []); -structure ThmDB = ThmDBFUN(); -structure Simplifier = SimplifierFUN(); -structure Readthy = ReadthyFUN(structure ThySyn = ThySyn and ThmDB = ThmDB - and Simplifier = Simplifier); +structure ThmDB = ThmDBFun(); +structure Readthy = ReadthyFun(structure ThySyn = ThySyn and ThmDB = ThmDB); open ThmDB Readthy; (* hide functors; saves space in PolyML *) functor ThyScanFun() = struct end; functor ThyParseFun() = struct end; +functor SimplifierFun() = struct end; fun init_thy_reader () = use_string - ["structure ThmDB = ThmDBFUN();", - "structure Simplifier = SimplifierFUN();", - "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \ - \and ThmDB = ThmDB \ - \and Simplifier = Simplifier);", + ["structure ThmDB = ThmDBFun();", + "structure Readthy = ReadthyFun(structure ThySyn = ThySyn \ + \and ThmDB = ThmDB);", "Readthy.loaded_thys := !loaded_thys;", "ThmDB.thm_db := !thm_db;", - "val first_init_readthy = false;", - "open Readthy ThmDB;"]; + "open ThmDB Readthy;"];