# HG changeset patch
# User wenzelm
# Date 897494181 -7200
# Node ID 9a67a024f4b809317f780ac924c637faf4c83966
# Parent  fc1a2421800f5f1b125395b74a54805a9b67470e
tuned transaction;

diff -r fc1a2421800f -r 9a67a024f4b8 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Jun 10 12:13:52 1998 +0200
+++ b/src/Pure/pure_thy.ML	Wed Jun 10 17:56:21 1998 +0200
@@ -342,10 +342,11 @@
       |> Theory.prep_ext
       |> Theory.add_name ("#" ^ name ^ ":" ^ string_of_int generation)  (* FIXME !!?? *)
       |> put_info {name = name, generation = generation + 1};
+    val (thy', opt_exn) = (transform_error f thy, None) handle exn => (thy, Some exn);
   in
-    (transform_error f thy, false, None) handle exn =>
-      if Sign.is_stale (Theory.sign_of thy) then (copy_thy, true, Some exn)
-      else (thy, false, Some exn)
+    if Sign.is_stale (Theory.sign_of thy') then
+      (copy_thy, true, opt_exn)
+    else (thy', false, opt_exn)
   end;