src/HOL/Tools/Function/function.ML

         lthy
         |> Local_Theory.declaration false (add_function_data o morph_function_data info)
       end
   in
     lthy
-    |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
+    |> Proof.theorem NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
     |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
   end
 
 val add_function =
   gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)

     |> ProofContext.note_thmss ""
        [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
     |> ProofContext.note_thmss ""
        [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
          [([Goal.norm_result termination], [])])] |> snd
-    |> Proof.theorem_i NONE afterqed [[(goal, [])]]
+    |> Proof.theorem NONE afterqed [[(goal, [])]]
   end
 
 val termination_proof = gen_termination_proof Syntax.check_term
 val termination_proof_cmd = gen_termination_proof Syntax.read_term