removed typedecl.ML (cf. object_logic.ML);
authorwenzelm
Wed Nov 28 16:44:22 2007 +0100 (2007-11-28)
changeset 254960a779502be57
parent 25495 98f3596bec44
child 25497 1c9b3733f887
removed typedecl.ML (cf. object_logic.ML);
src/Pure/IsaMakefile
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/IsaMakefile	Wed Nov 28 16:44:20 2007 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Wed Nov 28 16:44:22 2007 +0100
     1.3 @@ -73,7 +73,7 @@
     1.4    morphism.ML name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML		\
     1.5    proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML	\
     1.6    sorts.ML subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML theory.ML	\
     1.7 -  thm.ML type.ML typedecl.ML type_infer.ML unify.ML variable.ML
     1.8 +  thm.ML type.ML type_infer.ML unify.ML variable.ML
     1.9  	@./mk
    1.10  
    1.11  
     2.1 --- a/src/Pure/ROOT.ML	Wed Nov 28 16:44:20 2007 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Wed Nov 28 16:44:22 2007 +0100
     2.3 @@ -74,7 +74,6 @@
     2.4  use "conjunction.ML";
     2.5  use "assumption.ML";
     2.6  use "goal.ML";
     2.7 -use "typedecl.ML";
     2.8  use "axclass.ML";
     2.9  
    2.10  (*proof term operations*)