added Pure/term_subst.ML;
authorwenzelm
Tue Sep 12 12:12:33 2006 +0200 (2006-09-12)
changeset 20507bb68343f6f83
parent 20506 3ab3689c4a6e
child 20508 8182d961c7cc
added Pure/term_subst.ML;
src/Pure/IsaMakefile
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/IsaMakefile	Tue Sep 12 12:12:25 2006 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Tue Sep 12 12:12:33 2006 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4    install_pp.ML	library.ML logic.ML meta_simplifier.ML name.ML net.ML 		\
     1.5    old_goals.ML pattern.ML proof_general.ML proofterm.ML pure_thy.ML search.ML	\
     1.6    sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML 	\
     1.7 -  theory.ML thm.ML type.ML type_infer.ML variable.ML unify.ML
     1.8 +  term_subst.ML theory.ML thm.ML type.ML type_infer.ML variable.ML unify.ML
     1.9  	@./mk
    1.10  
    1.11  
     2.1 --- a/src/Pure/ROOT.ML	Tue Sep 12 12:12:25 2006 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Tue Sep 12 12:12:33 2006 +0200
     2.3 @@ -22,6 +22,7 @@
     2.4  (*fundamental structures*)
     2.5  use "name.ML";
     2.6  use "term.ML";
     2.7 +use "term_subst.ML";
     2.8  use "General/pretty.ML";
     2.9  use "sorts.ML";
    2.10  use "type.ML";