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