changeset 36323 | 655e2d74de3a |
parent 35897 | 8758895ea413 |
child 36610 | bafd82950e24 |
--- a/src/HOL/Tools/choice_specification.ML Sun Apr 25 15:13:33 2010 +0200 +++ b/src/HOL/Tools/choice_specification.ML Sun Apr 25 15:52:03 2010 +0200 @@ -226,7 +226,7 @@ in thy |> ProofContext.init - |> Proof.theorem_i NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]] + |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]] end;