# HG changeset patch
# User wenzelm
# Date 1208012442 -7200
# Node ID 6e93fbd4c96a123723a0dc25ce0658da347d95f7
# Parent  63306cb94313378d0584f9f1b2443b4694b004ed
removed obsolete compress.ML

diff -r 63306cb94313 -r 6e93fbd4c96a src/Pure/IsaMakefile
--- 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	\
diff -r 63306cb94313 -r 6e93fbd4c96a src/Pure/ROOT.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";