# HG changeset patch
# User wenzelm
# Date 1256645704 -3600
# Node ID 5bb809208876ba827d172a1eab740030f15c9dd4
# Parent  11a1af478dac0fd69ad00ba672de0ed977c83524
tuned;

diff -r 11a1af478dac -r 5bb809208876 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Tue Oct 27 11:25:56 2009 +0100
+++ b/src/Pure/Thy/thy_load.ML	Tue Oct 27 13:15:04 2009 +0100
@@ -41,16 +41,22 @@
 
 fun show_path () = map Path.implode (! load_path);
 
-fun del_path s = CRITICAL (fn () =>
-    Unsynchronized.change load_path (remove (op =) (Path.explode s)));
-fun add_path s = CRITICAL (fn () =>
-    (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
-fun path_add s = CRITICAL (fn () =>
+fun del_path s =
+  CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s)));
+
+fun add_path s =
+  CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
+
+fun path_add s =
+  CRITICAL (fn () =>
     (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
+
 fun reset_path () = load_path := [Path.current];
 
 fun with_paths ss f x =
-  CRITICAL (fn () => setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x);
+  CRITICAL (fn () =>
+    setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x);
+
 fun with_path s f x = with_paths [s] f x;
 
 fun search_path dir path =