theorem: apply hook last;
authorwenzelm
Fri Sep 07 22:13:49 2007 +0200 (2007-09-07)
changeset 2455757e2a5fbde86
parent 24556 22ac3c8d78a5
child 24558 419f7cde7f59
theorem: apply hook last;
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/specification.ML	Fri Sep 07 22:13:48 2007 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Fri Sep 07 22:13:49 2007 +0200
     1.3 @@ -289,8 +289,8 @@
     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 +    |> Proof.refine_insert facts
     1.8      |> Library.apply (map (fn (f, _) => f int) (rev (TheoremHook.get (Context.Proof goal_ctxt))))
     1.9 -    |> Proof.refine_insert facts
    1.10    end;
    1.11  
    1.12  in