diff -r 0fffc66b10d7 -r ac7570d80c3d src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Mar 28 17:10:43 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Mar 28 17:21:11 2009 +0100
@@ -327,7 +327,7 @@
         val (facts, goal_ctxt) = elems_ctxt
           |> (snd o ProofContext.add_fixes_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
           |> fold_map assume_case (obtains ~~ propp)
-          |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
+          |-> (fn ths => ProofContext.note_thmss Thm.assumptionK
                 [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
       in ((prems, stmt, facts), goal_ctxt) end);
 
@@ -370,7 +370,7 @@
       end;
   in
     goal_ctxt
-    |> ProofContext.note_thmss_i Thm.assumptionK
+    |> ProofContext.note_thmss Thm.assumptionK
       [((Binding.name AutoBind.assmsN, []), [(prems, [])])]
     |> snd
     |> Proof.theorem_i before_qed after_qed' (map snd stmt)