removed typedecl.ML (cf. object_logic.ML);
--- a/src/Pure/IsaMakefile Wed Nov 28 16:44:20 2007 +0100
+++ b/src/Pure/IsaMakefile Wed Nov 28 16:44:22 2007 +0100
@@ -73,7 +73,7 @@
morphism.ML name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML \
proofterm.ML pure_setup.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 typedecl.ML type_infer.ML unify.ML variable.ML
+ thm.ML type.ML type_infer.ML unify.ML variable.ML
@./mk
--- a/src/Pure/ROOT.ML Wed Nov 28 16:44:20 2007 +0100
+++ b/src/Pure/ROOT.ML Wed Nov 28 16:44:22 2007 +0100
@@ -74,7 +74,6 @@
use "conjunction.ML";
use "assumption.ML";
use "goal.ML";
-use "typedecl.ML";
use "axclass.ML";
(*proof term operations*)