diff -r 22ac3c8d78a5 -r 57e2a5fbde86 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Sep 07 22:13:48 2007 +0200
+++ b/src/Pure/Isar/specification.ML	Fri Sep 07 22:13:49 2007 +0200
@@ -289,8 +289,8 @@
     |> ProofContext.note_thmss_i Thm.assumptionK [((AutoBind.assmsN, []), [(prems, [])])]
     |> snd
     |> Proof.theorem_i before_qed after_qed' (map snd stmt)
+    |> Proof.refine_insert facts
     |> Library.apply (map (fn (f, _) => f int) (rev (TheoremHook.get (Context.Proof goal_ctxt))))
-    |> Proof.refine_insert facts
   end;
 
 in