# HG changeset patch
# User wenzelm
# Date 1350392569 -7200
# Node ID fb2d8ba7d3a9f54b2e4f2e0d2e24ff2b34988259
# Parent  4e49ac1c8a6c634f8bc105b854bb999bbfd29623
more friendly handling of Pure.thy bootstrap errors;

diff -r 4e49ac1c8a6c -r fb2d8ba7d3a9 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Oct 16 14:14:37 2012 +0200
+++ b/src/Pure/ROOT.ML	Tue Oct 16 15:02:49 2012 +0200
@@ -305,17 +305,6 @@
 use "ProofGeneral/proof_general_emacs.ML";
 
 
-(* the Pure theory *)
-
-use "pure_syn.ML";
-Thy_Info.use_thy ("Pure", Position.none);
-Context.set_thread_data NONE;
-structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
-
-
-use "ProofGeneral/pgip_tests.ML";
-
-
 (* ML toplevel pretty printing *)
 
 toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
@@ -326,7 +315,6 @@
 toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
 toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
 toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
-toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
 toplevel_pp ["Context", "theory"] "Context.pretty_thy";
 toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
@@ -339,6 +327,18 @@
 if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
 
 
+(* the Pure theory *)
+
+use "pure_syn.ML";
+Toplevel.program (fn () => Thy_Info.use_thy ("Pure", Position.none));
+Context.set_thread_data NONE;
+structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
+
+toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
+
+use "ProofGeneral/pgip_tests.ML";
+
+
 (* ML toplevel commands *)
 
 fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));