# HG changeset patch
# User wenzelm
# Date 1158055953 -7200
# Node ID bb68343f6f83e3af91e43508adb01b76ef49b0cf
# Parent  3ab3689c4a6ee6be2506c3a1ec98893346796bb7
added Pure/term_subst.ML;

diff -r 3ab3689c4a6e -r bb68343f6f83 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Sep 12 12:12:25 2006 +0200
+++ b/src/Pure/IsaMakefile	Tue Sep 12 12:12:33 2006 +0200
@@ -69,7 +69,7 @@
   install_pp.ML	library.ML logic.ML meta_simplifier.ML name.ML net.ML 		\
   old_goals.ML pattern.ML proof_general.ML proofterm.ML pure_thy.ML search.ML	\
   sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML 	\
-  theory.ML thm.ML type.ML type_infer.ML variable.ML unify.ML
+  term_subst.ML theory.ML thm.ML type.ML type_infer.ML variable.ML unify.ML
 	@./mk
 
 
diff -r 3ab3689c4a6e -r bb68343f6f83 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Sep 12 12:12:25 2006 +0200
+++ b/src/Pure/ROOT.ML	Tue Sep 12 12:12:33 2006 +0200
@@ -22,6 +22,7 @@
 (*fundamental structures*)
 use "name.ML";
 use "term.ML";
+use "term_subst.ML";
 use "General/pretty.ML";
 use "sorts.ML";
 use "type.ML";