src/Pure/Isar/specification.ML

         val stmt = [((Binding.empty, atts), [(thesis, [])])];
 
         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);
 
 structure TheoremHook = GenericDataFun
 (

             in lthy'' end)
         |> after_qed results'
       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)
     |> Proof.refine_insert facts
     |> Library.apply (map (fn (f, _) => f int) (rev (TheoremHook.get (Context.Proof goal_ctxt))))