# HG changeset patch
# User wenzelm
# Date 1344422321 -7200
# Node ID f04320479ff923a9fc80b6636c44c3b9b85397fe
# Parent  a45ba78abcc1e901f3589a37d2d661253ade48ec
simplified Pure bootstrap -- separate pure_setup.ML was required for Alice/ML at some point;

diff -r a45ba78abcc1 -r f04320479ff9 src/Pure/ROOT
--- a/src/Pure/ROOT	Wed Aug 08 12:33:40 2012 +0200
+++ b/src/Pure/ROOT	Wed Aug 08 12:38:41 2012 +0200
@@ -226,7 +226,6 @@
     "pattern.ML"
     "primitive_defs.ML"
     "proofterm.ML"
-    "pure_setup.ML"
     "pure_thy.ML"
     "raw_simplifier.ML"
     "search.ML"
diff -r a45ba78abcc1 -r f04320479ff9 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Aug 08 12:33:40 2012 +0200
+++ b/src/Pure/ROOT.ML	Wed Aug 08 12:38:41 2012 +0200
@@ -303,7 +303,59 @@
 use "ProofGeneral/proof_general_emacs.ML";
 
 
-use "pure_setup.ML";
+(* ML toplevel use commands *)
+
+fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
+
+fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
+fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
+
+
+(* the Pure theory *)
+
+val _ =
+  Outer_Syntax.command
+    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.none) "begin theory context"
+    (Thy_Header.args >> (fn header =>
+      Toplevel.print o
+        Toplevel.init_theory
+          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
+
+Unsynchronized.setmp Multithreading.max_threads 1
+  use_thy "Pure";
+Context.set_thread_data NONE;
+
+structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
+
+
+(* ML toplevel pretty printing *)
+
+toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
+toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
+toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
+toplevel_pp ["Position", "T"] "Pretty.position";
+toplevel_pp ["Binding", "binding"] "Pretty.str o Binding.print";
+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";
+toplevel_pp ["Ast", "ast"] "Ast.pretty_ast";
+toplevel_pp ["Path", "T"] "Path.pretty";
+toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
+toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
+toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
+
+if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
+
+
+(* misc *)
+
+val cd = File.cd o Path.explode;
+
+Proofterm.proofs := 0;
 
 use "ProofGeneral/pgip_tests.ML";
 
diff -r a45ba78abcc1 -r f04320479ff9 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Wed Aug 08 12:33:40 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(*  Title:      Pure/pure_setup.ML
-    Author:     Makarius
-
-Pure theory and ML toplevel setup.
-*)
-
-(* ML toplevel use commands *)
-
-fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
-
-fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
-fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
-
-
-(* the Pure theory *)
-
-val _ =
-  Outer_Syntax.command
-    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.none) "begin theory context"
-    (Thy_Header.args >> (fn header =>
-      Toplevel.print o
-        Toplevel.init_theory
-          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
-
-Unsynchronized.setmp Multithreading.max_threads 1
-  use_thy "Pure";
-Context.set_thread_data NONE;
-
-structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
-
-
-(* ML toplevel pretty printing *)
-
-toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
-toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
-toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
-toplevel_pp ["Position", "T"] "Pretty.position";
-toplevel_pp ["Binding", "binding"] "Pretty.str o Binding.print";
-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";
-toplevel_pp ["Ast", "ast"] "Ast.pretty_ast";
-toplevel_pp ["Path", "T"] "Path.pretty";
-toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
-toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
-toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
-
-if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
-
-
-(* misc *)
-
-val cd = File.cd o Path.explode;
-
-Proofterm.proofs := 0;
-