--- a/src/Pure/Isar/specification.ML Sun Apr 25 15:13:33 2010 +0200
+++ b/src/Pure/Isar/specification.ML Sun Apr 25 15:52:03 2010 +0200
@@ -403,7 +403,7 @@
goal_ctxt
|> ProofContext.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
|> snd
- |> Proof.theorem_i before_qed after_qed' (map snd stmt)
+ |> Proof.theorem before_qed after_qed' (map snd stmt)
|> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
|> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
error "Illegal schematic goal statement")