# HG changeset patch
# User wenzelm
# Date 1206625273 -3600
# Node ID f33d1b522316c02b67a331f8373663689697b6f9
# Parent  ddac7ef1e991346f6af4933f64aa0d347be1a564
implicit setup of emerging theory Pure;

diff -r ddac7ef1e991 -r f33d1b522316 src/Pure/compress.ML
--- a/src/Pure/compress.ML	Thu Mar 27 14:41:12 2008 +0100
+++ b/src/Pure/compress.ML	Thu Mar 27 14:41:13 2008 +0100
@@ -9,7 +9,6 @@
 
 signature COMPRESS =
 sig
-  val init_data: theory -> theory
   val typ: theory -> typ -> typ
   val term: theory -> term -> term
 end;
@@ -31,7 +30,7 @@
     ref (Termtab.merge (K true) (terms1, terms2)));
 );
 
-val init_data = CompressData.init;
+val _ = Context.>> CompressData.init;
 
 
 (* compress types *)
diff -r ddac7ef1e991 -r f33d1b522316 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Thu Mar 27 14:41:12 2008 +0100
+++ b/src/Pure/pure_setup.ML	Thu Mar 27 14:41:13 2008 +0100
@@ -16,8 +16,11 @@
 
 (* the Pure theories *)
 
-use_thy "Pure";
-structure Pure = struct val thy = theory "Pure" end;
+Context.>> (OuterSyntax.process_file (Path.explode "Pure.thy"));
+Context.>> Theory.end_theory;
+structure Pure = struct val thy = ML_Context.the_global_context () end;
+Context.set_thread_data NONE;
+ThyInfo.register_theory Pure.thy;
 
 Context.add_setup
  (Sign.del_modesyntax_i Syntax.mode_default PureThy.appl_syntax #>