1.1 --- a/src/Pure/ROOT.ML	Tue Oct 16 14:14:37 2012 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Tue Oct 16 15:02:49 2012 +0200
     1.3 @@ -305,17 +305,6 @@
     1.4  use "ProofGeneral/proof_general_emacs.ML";
     1.5  
     1.6  
     1.7 -(* the Pure theory *)
     1.8 -
     1.9 -use "pure_syn.ML";
    1.10 -Thy_Info.use_thy ("Pure", Position.none);
    1.11 -Context.set_thread_data NONE;
    1.12 -structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
    1.13 -
    1.14 -
    1.15 -use "ProofGeneral/pgip_tests.ML";
    1.16 -
    1.17 -
    1.18  (* ML toplevel pretty printing *)
    1.19  
    1.20  toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
    1.21 @@ -326,7 +315,6 @@
    1.22  toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
    1.23  toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
    1.24  toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
    1.25 -toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
    1.26  toplevel_pp ["Context", "theory"] "Context.pretty_thy";
    1.27  toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
    1.28  toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
    1.29 @@ -339,6 +327,18 @@
    1.30  if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
    1.31  
    1.32  
    1.33 +(* the Pure theory *)
    1.34 +
    1.35 +use "pure_syn.ML";
    1.36 +Toplevel.program (fn () => Thy_Info.use_thy ("Pure", Position.none));
    1.37 +Context.set_thread_data NONE;
    1.38 +structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
    1.39 +
    1.40 +toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
    1.41 +
    1.42 +use "ProofGeneral/pgip_tests.ML";
    1.43 +
    1.44 +
    1.45  (* ML toplevel commands *)
    1.46  
    1.47  fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));