# HG changeset patch
# User wenzelm
# Date 1126973487 -7200
# Node ID 2e9f745924d0514ee8180681a3c533affe423b29
# Parent  92d36be64b46d5ce06f6a64ec8daec3d1bb7b10d
removed obsolete BasisLibrary;
proof_general.ML: setmp proofs 1 to capture sane default preferences;

diff -r 92d36be64b46 -r 2e9f745924d0 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Sep 17 18:11:26 2005 +0200
+++ b/src/Pure/ROOT.ML	Sat Sep 17 18:11:27 2005 +0200
@@ -89,31 +89,18 @@
 (*the IsaPlanner subsystem*)
 cd "IsaPlanner"; use "ROOT.ML"; cd "..";
 
+cd "Tools"; use "ROOT.ML"; cd "..";
+
 (*configuration for Proof General*)
-use "proof_general.ML";
-
-cd "Tools"; use "ROOT.ML"; cd "..";
+setmp proofs 1 use "proof_general.ML";
 
 use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end;
 use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end;
 
-
-(*several object-logics declare theories that hide basis library structures*)
-structure BasisLibrary =
-struct
-  structure List = List;
-  structure Option = Option;
-  structure Bool = Bool;
-  structure String = String;
-  structure Int = Int;
-  structure Real = Real;
-end;
-
+(*final ML setup*)
 use "install_pp.ML";
-
 val use = ThyInfo.use;
 val cd = File.cd o Path.unpack;
-
 ml_prompts "ML> " "ML# ";
 
 proofs := 0;