diff -r 89104dca628e -r 944f80576be0 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Tue Nov 21 18:07:29 2006 +0100
+++ b/src/HOL/Tools/specification_package.ML	Tue Nov 21 18:07:30 2006 +0100
@@ -228,7 +228,7 @@
     in
       thy
       |> ProofContext.init
-      |> Proof.theorem_i PureThy.internalK NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
+      |> Proof.theorem_i NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
     end;