src/HOL/Tools/record_package.ML

   let
     val cert = cterm_of (Thm.theory_of_thm st);
     val g = nth (prems_of st) (i - 1);
     val params = Logic.strip_params g;
     val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
-    val rule' = Thm.lift_rule (Thm.cgoal_of st i) rule;
+    val rule' = Thm.lift_rule (Thm.cprem_of st i) rule;
     val (P, ys) = strip_comb (HOLogic.dest_Trueprop
       (Logic.strip_assums_concl (prop_of rule')));
     (* ca indicates if rule is a case analysis or induction rule *)
     val (x, ca) = (case rev (Library.drop (length params, ys)) of
         [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop

 fun ex_inst_tac i st =
   let
     val sg = sign_of_thm st;
     val g = nth (prems_of st) (i - 1);
     val params = Logic.strip_params g;
-    val exI' = Thm.lift_rule (Thm.cgoal_of st i) exI;
+    val exI' = Thm.lift_rule (Thm.cprem_of st i) exI;
     val (_$(_$x)) = Logic.strip_assums_concl (hd (prems_of exI'));
     val cx = cterm_of sg (fst (strip_comb x));
 
   in Seq.single (Library.foldl (fn (st,v) =>
         Seq.hd