src/HOL/Tools/specification_package.ML

 fun add_specification axiomatic cos arg =
     arg |> apsnd Thm.freezeT
         |> 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 *)
 
 fun collect_consts (        t $ u,tms) = collect_consts (u,collect_consts (t,tms))
   | collect_consts (   Abs(_,_,t),tms) = collect_consts (t,tms)

                         else ()
             in
                 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 *)
 
 local structure P = OuterParse and K = OuterKeyword in