diff -r a37d39fe32f8 -r d07959fabde6 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Thu Aug 26 12:06:00 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Thu Aug 26 13:09:12 2010 +0200
@@ -220,8 +220,8 @@
                     |> process_all (zip3 alt_names rew_imps frees)
             end
 
-      fun after_qed [[thm]] = (ProofContext.theory (fn thy =>
-        #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm)))));
+      fun after_qed [[thm]] = ProofContext.background_theory (fn thy =>
+        #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm))));
     in
       thy
       |> ProofContext.init_global