theorem: apply hook last;
authorwenzelm
Fri, 07 Sep 2007 22:13:49 +0200
changeset 24557 57e2a5fbde86
parent 24556 22ac3c8d78a5
child 24558 419f7cde7f59
theorem: apply hook last;
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