src/HOL/Tools/specification_package.ML
changeset 21434 944f80576be0
parent 21359 072e83a0b5bb
child 21858 05f57309170c
--- 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;