1.1 --- a/src/Pure/IsaMakefile	Mon Feb 26 23:18:24 2007 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Mon Feb 26 23:18:26 2007 +0100
     1.3 @@ -66,10 +66,10 @@
     1.4    Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML compress.ML		\
     1.5    conjunction.ML consts.ML context.ML defs.ML display.ML drule.ML envir.ML	\
     1.6    fact_index.ML goal.ML install_pp.ML library.ML logic.ML meta_simplifier.ML 	\
     1.7 -  morphism.ML name.ML net.ML old_goals.ML pattern.ML proofterm.ML pure_thy.ML	\
     1.8 -  search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML 	\
     1.9 -  term.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML 	\
    1.10 -  variable.ML
    1.11 +  more_thm.ML morphism.ML name.ML net.ML old_goals.ML pattern.ML proofterm.ML   \
    1.12 +  pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML     \
    1.13 +  tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML       \
    1.14 +  unify.ML variable.ML
    1.15  	@./mk
    1.16  
    1.17  

     2.1 --- a/src/Pure/ROOT.ML	Mon Feb 26 23:18:24 2007 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Mon Feb 26 23:18:26 2007 +0100
     2.3 @@ -47,6 +47,7 @@
     2.4  use "theory.ML";
     2.5  use "proofterm.ML";
     2.6  use "thm.ML";
     2.7 +use "more_thm.ML";
     2.8  use "fact_index.ML";
     2.9  use "pure_thy.ML";
    2.10  use "display.ML";