attribute: Context.mapping;
Proof.theorem_i;

--- a/src/HOL/Tools/specification_package.ML	Mon Oct 09 02:19:54 2006 +0200
+++ b/src/HOL/Tools/specification_package.ML	Mon Oct 09 02:19:55 2006 +0200
@@ -87,9 +87,6 @@
         |> proc_exprop axiomatic cos
         |> apsnd standard
 
-fun add_spec x y (context, thm) =
-  (Context.the_theory context, thm) |> add_specification x y |>> Context.Theory;
-
 
 (* Collect all intances of constants in term *)
 
@@ -225,13 +222,15 @@
                 arg |> apsnd Thm.freezeT
                     |> process_all (zip3 alt_names rew_imps frees)
             end
-            fun post_proc (context, th) =
-                post_process (Context.theory_of context, th) |>> Context.Theory;
+
+      fun after_qed [[thm]] = ProofContext.theory (fn thy =>
+        #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm))));
     in
-      IsarThy.theorem_i PureThy.internalK
-        ("", [add_spec axiomatic (zip3 names cnames overloaded), post_proc])
-        (HOLogic.mk_Trueprop ex_prop, []) thy
-    end
+      thy
+      |> ProofContext.init
+      |> Proof.theorem_i PureThy.internalK NONE after_qed
+        (SOME "") ("", []) [(("", []), [(HOLogic.mk_Trueprop ex_prop, [])])]
+    end;
 
 
 (* outer syntax *)