changeset 18784 | 2d93559db27e |
parent 18728 | 6790126ab5f6 |
child 18808 | 838fb803636e |
--- a/src/Pure/Isar/proof.ML Wed Jan 25 00:21:41 2006 +0100 +++ b/src/Pure/Isar/proof.ML Wed Jan 25 00:21:42 2006 +0100 @@ -858,7 +858,7 @@ fun after_qed' results = (case target of NONE => I | SOME prfx => store_results (NameSpace.base prfx) - (map (map (ProofContext.export ctxt thy_ctxt + (map (map (ProofContext.export_standard ctxt thy_ctxt #> Drule.strip_shyps_warning)) results)) #> after_qed results; in