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