src/HOLCF/Tools/pcpodef.ML

     val args = map (apsnd (prep_constraint ctxt)) raw_args;
     val (goal1, goal2, make_result) =
       prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
     fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
       | after_qed _ = raise Fail "cpodef_proof";
-  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
+  in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
 
 fun gen_pcpodef_proof prep_term prep_constraint
     ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
   let
     val ctxt = ProofContext.init thy;
     val args = map (apsnd (prep_constraint ctxt)) raw_args;
     val (goal1, goal2, make_result) =
       prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
     fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
       | after_qed _ = raise Fail "pcpodef_proof";
-  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
+  in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
 
 in
 
 fun cpodef_proof x = gen_cpodef_proof Syntax.check_term (K I) x;
 fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term Typedecl.read_constraint x;