# HG changeset patch
# User wenzelm
# Date 1279800103 -7200
# Node ID 0cf799737f5f886d6586559b972ae16855b1d86b
# Parent  332cd0197d34ac17562d6381b287125f400104d2
tuned;

diff -r 332cd0197d34 -r 0cf799737f5f src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Jul 22 10:41:12 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Jul 22 14:01:43 2010 +0200
@@ -578,7 +578,9 @@
 
 (* post-transition hooks *)
 
-local val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list) in
+local
+  val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list);
+in
 
 fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
 fun get_hooks () = ! hooks;
@@ -597,9 +599,10 @@
       fun do_profiling f x = profile (! profiling) f x;
 
       val (result, status) =
-         state |> (apply_trans int trans
-          |> (if ! profiling > 0 andalso not no_timing then do_profiling else I)
-          |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
+         state |>
+          (apply_trans int trans
+            |> (! profiling > 0 andalso not no_timing) ? do_profiling
+            |> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing);
 
       val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
     in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end);
diff -r 332cd0197d34 -r 0cf799737f5f src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Jul 22 10:41:12 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Jul 22 14:01:43 2010 +0200
@@ -105,10 +105,8 @@
 fun base_name s = Path.implode (Path.base (Path.explode s));
 
 
-type thy = deps option * theory option;
-
 local
-  val database = Unsynchronized.ref (Graph.empty: thy Graph.T);
+  val database = Unsynchronized.ref (Graph.empty: (deps option * theory option) Graph.T);
 in
   fun get_thys () = ! database;
   fun change_thys f = CRITICAL (fn () => Unsynchronized.change database f);
@@ -421,9 +419,11 @@
 
 fun check_ml master (src_path, info) =
   let val info' =
-    (case info of NONE => NONE
+    (case info of
+      NONE => NONE
     | SOME (_, id) =>
-        (case Thy_Load.check_ml (master_dir master) src_path of NONE => NONE
+        (case Thy_Load.check_ml (master_dir master) src_path of
+          NONE => NONE
         | SOME (path', id') => if id <> id' then NONE else SOME (path', id')))
   in (src_path, info') end;