--- a/src/Pure/Isar/specification.ML Thu Sep 06 11:53:17 2007 +0200
+++ b/src/Pure/Isar/specification.ML Thu Sep 06 12:30:11 2007 +0200
@@ -289,8 +289,7 @@
|> ProofContext.note_thmss_i Thm.assumptionK [((AutoBind.assmsN, []), [(prems, [])])]
|> snd
|> Proof.theorem_i before_qed after_qed' (map snd stmt)
- |> Library.apply (map (fn (f, _) => f int)
- (TheoremHook.get (Context.Proof goal_ctxt)))
+ |> Library.apply (map (fn (f, _) => f int) (rev (TheoremHook.get (Context.Proof goal_ctxt))))
|> Proof.refine_insert facts
end;