removed obsolete compress.ML
authorwenzelm
Sat, 12 Apr 2008 17:00:42 +0200
changeset 26629 6e93fbd4c96a
parent 26628 63306cb94313
child 26630 3074b3de4f4f
removed obsolete compress.ML
src/Pure/IsaMakefile
src/Pure/ROOT.ML
--- a/src/Pure/IsaMakefile	Sat Apr 12 17:00:40 2008 +0200
+++ b/src/Pure/IsaMakefile	Sat Apr 12 17:00:42 2008 +0200
@@ -71,10 +71,10 @@
   Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML	\
   Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML			\
   Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML	\
-  assumption.ML axclass.ML codegen.ML compress.ML config.ML		\
-  conjunction.ML consts.ML context.ML conv.ML defs.ML display.ML	\
-  drule.ML envir.ML facts.ML goal.ML interpretation.ML library.ML	\
-  logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML	\
+  assumption.ML axclass.ML codegen.ML config.ML conjunction.ML		\
+  consts.ML context.ML conv.ML defs.ML display.ML drule.ML envir.ML	\
+  facts.ML goal.ML interpretation.ML library.ML logic.ML		\
+  meta_simplifier.ML more_thm.ML 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	\
--- a/src/Pure/ROOT.ML	Sat Apr 12 17:00:40 2008 +0200
+++ b/src/Pure/ROOT.ML	Sat Apr 12 17:00:42 2008 +0200
@@ -34,7 +34,6 @@
 use "type.ML";
 use "type_infer.ML";
 use "config.ML";
-use "compress.ML";
 
 (*inner syntax module*)
 use "Syntax/ast.ML";