# HG changeset patch
# User wenzelm
# Date 897314270 -7200
# Node ID cf4e3b487caf915d0e1533b72e8a6f36e2cc772f
# Parent  f73ad32e44d3f4ea080cb668800feea348c21d0c
added theory_data.ML;

diff -r f73ad32e44d3 -r cf4e3b487caf src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Mon Jun 08 15:57:30 1998 +0200
+++ b/src/Pure/IsaMakefile	Mon Jun 08 15:57:50 1998 +0200
@@ -36,7 +36,7 @@
   drule.ML envir.ML goals.ML install_pp.ML library.ML logic.ML \
   name_space.ML net.ML object.ML pattern.ML pure_thy.ML search.ML \
   seq.ML sign.ML sorts.ML table.ML tactic.ML tctical.ML term.ML \
-  theory.ML thm.ML type.ML type_infer.ML unify.ML
+  theory.ML theory_data.ML thm.ML type.ML type_infer.ML unify.ML
 	@./mk
 
 
diff -r f73ad32e44d3 -r cf4e3b487caf src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Jun 08 15:57:30 1998 +0200
+++ b/src/Pure/ROOT.ML	Mon Jun 08 15:57:50 1998 +0200
@@ -37,6 +37,7 @@
 use "net.ML";
 use "logic.ML";
 use "theory.ML";
+use "theory_data.ML";
 use "thm.ML";
 use "display.ML";
 use "attribute.ML";