# HG changeset patch
# User wenzelm
# Date 1189074611 -7200
# Node ID f13c59e40617a14147afc4c56b90f276fec8b8a0
# Parent  98c978a42a42f4df0e489b4005e96a2ca2a3a7fc
theorem hooks: apply in declaration order;

diff -r 98c978a42a42 -r f13c59e40617 src/Pure/Isar/specification.ML
--- 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;