src/HOL/Tools/Datatype/datatype_data.ML

         #-> after_qed
       end;
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules))
+    |> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules))
   end;
 
 val rep_datatype = gen_rep_datatype Sign.cert_term;
 val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);