# HG changeset patch
# User wenzelm
# Date 1139534543 -3600
# Node ID 0ded3b84287827e71326e41e7c2f409d6ee3e753
# Parent  a203cd5107e0319231ed79c17148beb67df46555
use proof_general.ML: setmp quick_and_dirty captures default value;

diff -r a203cd5107e0 -r 0ded3b842878 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Feb 10 02:22:21 2006 +0100
+++ b/src/Pure/ROOT.ML	Fri Feb 10 02:22:23 2006 +0100
@@ -87,14 +87,16 @@
 cd "Tools"; use "ROOT.ML"; cd "..";
 
 (*configuration for Proof General*)
-setmp proofs 1 use "proof_general.ML";
+(use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general.ML";
 
-use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end;
+use_thy "Pure";
+structure Pure = struct val thy = theory "Pure" end;
 
 Context.add_setup
  (Theory.del_modesyntax Syntax.default_mode Syntax.appl_syntax #>
   Theory.add_syntax Syntax.applC_syntax);
-use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end;
+use_thy "CPure";
+structure CPure = struct val thy = theory "CPure" end;
 
 (*final ML setup*)
 use "install_pp.ML";