# HG changeset patch
# User wenzelm
# Date 1196264662 -3600
# Node ID 0a779502be5731cc6479da74df26856d54abd260
# Parent  98f3596bec4474039aa9c8560c24b14fb654986b
removed typedecl.ML (cf. object_logic.ML);

diff -r 98f3596bec44 -r 0a779502be57 src/Pure/IsaMakefile
--- 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
 
 
diff -r 98f3596bec44 -r 0a779502be57 src/Pure/ROOT.ML
--- 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*)