added Pure/term_subst.ML;
authorwenzelm
Tue, 12 Sep 2006 12:12:33 +0200
changeset 20507 bb68343f6f83
parent 20506 3ab3689c4a6e
child 20508 8182d961c7cc
added Pure/term_subst.ML;
src/Pure/IsaMakefile
src/Pure/ROOT.ML
--- 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
 
 
--- 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";