# HG changeset patch # User wenzelm # Date 877705654 -7200 # Node ID d788dcb86930031f8ad7031388238193a2c157c1 # Parent 173fcf95412f4999de5781c8f257868192db70e3 added pure_thy.ML; diff -r 173fcf95412f -r d788dcb86930 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Fri Oct 24 17:06:45 1997 +0200 +++ b/src/Pure/IsaMakefile Fri Oct 24 17:07:34 1997 +0200 @@ -17,7 +17,7 @@ Thy/symbol_input.ML Thy/thm_database.ML Thy/thy_parse.ML Thy/thy_read.ML \ Thy/thy_scan.ML Thy/thy_syn.ML Thy/thy_info.ML Thy/browser_info.ML \ axclass.ML basis.ML data.ML deriv.ML display.ML drule.ML envir.ML goals.ML \ - install_pp.ML library.ML logic.ML net.ML name_space.ML pattern.ML \ + install_pp.ML library.ML logic.ML net.ML name_space.ML pattern.ML pure_thy.ML \ search.ML section_utils.ML sequence.ML sign.ML sorts.ML symtab.ML tactic.ML \ tctical.ML term.ML theory.ML thm.ML type.ML type_infer.ML unify.ML diff -r 173fcf95412f -r d788dcb86930 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Oct 24 17:06:45 1997 +0200 +++ b/src/Pure/ROOT.ML Fri Oct 24 17:07:34 1997 +0200 @@ -39,8 +39,9 @@ use "logic.ML"; use "theory.ML"; use "thm.ML"; +use "display.ML"; +use "pure_thy.ML"; use "deriv.ML"; -use "display.ML"; use "drule.ML"; use "tctical.ML"; use "search.ML"; @@ -48,9 +49,6 @@ use "goals.ML"; use "axclass.ML"; -structure Pure = struct val thy = Theory.pure end; -structure CPure = struct val thy = Theory.cpure end; - (*Theory parser and loader*) cd "Thy"; use "ROOT.ML";