--- a/src/Pure/IsaMakefile Mon Feb 26 23:18:24 2007 +0100
+++ b/src/Pure/IsaMakefile Mon Feb 26 23:18:26 2007 +0100
@@ -66,10 +66,10 @@
Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML compress.ML \
conjunction.ML consts.ML context.ML defs.ML display.ML drule.ML envir.ML \
fact_index.ML goal.ML install_pp.ML library.ML logic.ML meta_simplifier.ML \
- morphism.ML name.ML net.ML old_goals.ML pattern.ML proofterm.ML pure_thy.ML \
- search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML \
- term.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML \
- variable.ML
+ more_thm.ML morphism.ML name.ML net.ML old_goals.ML pattern.ML proofterm.ML \
+ pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML \
+ tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML \
+ unify.ML variable.ML
@./mk
--- a/src/Pure/ROOT.ML Mon Feb 26 23:18:24 2007 +0100
+++ b/src/Pure/ROOT.ML Mon Feb 26 23:18:26 2007 +0100
@@ -47,6 +47,7 @@
use "theory.ML";
use "proofterm.ML";
use "thm.ML";
+use "more_thm.ML";
use "fact_index.ML";
use "pure_thy.ML";
use "display.ML";