src/Pure/Isar/class_target.ML

     fun after_qed results =
       ProofContext.theory ((fold o fold) AxClass.add_classrel results);
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed [[(mk_prop thy classrel, [])]]
+    |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
   end;
 
 in
 
 val classrel =

     lthy
     |> do_proof after_qed' arities_proof
   end;
 
 val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts =>
-  Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
+  Proof.theorem NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
 
 fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
   fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
     (fn {context, ...} => tac context)) ts) lthy) I;
 

     fun after_qed results = ProofContext.theory
       ((fold o fold) AxClass.add_arity results);
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed (map (fn t => [(t, [])]) arities)
+    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
   end;
 
 
 (** tactics and methods **)