removed typedecl.ML (cf. object_logic.ML);
authorwenzelm
Wed, 28 Nov 2007 16:44:22 +0100
changeset 25496 0a779502be57
parent 25495 98f3596bec44
child 25497 1c9b3733f887
removed typedecl.ML (cf. object_logic.ML);
src/Pure/IsaMakefile
src/Pure/ROOT.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*)