changeset 21359 | 072e83a0b5bb |
parent 21116 | be58cded79da |
child 21434 | 944f80576be0 |
--- a/src/HOL/Tools/specification_package.ML Tue Nov 14 15:29:50 2006 +0100 +++ b/src/HOL/Tools/specification_package.ML Tue Nov 14 15:29:52 2006 +0100 @@ -228,8 +228,7 @@ in thy |> ProofContext.init - |> Proof.theorem_i PureThy.internalK NONE after_qed - (SOME "") ("", []) [(("", []), [(HOLogic.mk_Trueprop ex_prop, [])])] + |> Proof.theorem_i PureThy.internalK NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]] end;