src/HOL/Tools/Function/size.ML

       HOLogic.mk_eq (app fs r $ Free p,
         the (size_of_type tab extra_size size_ofp T) $ Free p);
 
     fun prove_unfolded_size_eqs size_ofp fs =
       if null recTs2 then []
-      else Datatype_Aux.split_conj_thm (Skip_Proof.prove ctxt xs []
+      else Datatype_Aux.split_conj_thm (Goal.prove_sorry ctxt xs []
         (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (replicate l @{term True} @
            map (mk_unfolded_size_eq (AList.lookup op =
                (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
              (xs ~~ recTs2 ~~ rec_combs2))))
         (fn _ => (Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1));

     val simpset3 = HOL_basic_ss addsimps
       rec_rewrites @ size_def_thms' @ unfolded_size_eqs2;
 
     fun prove_size_eqs p size_fns size_ofp simpset =
       maps (fn (((_, (_, _, constrs)), size_const), T) =>
-        map (fn constr => Drule.export_without_context (Skip_Proof.prove ctxt [] []
+        map (fn constr => Drule.export_without_context (Goal.prove_sorry ctxt [] []
           (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
              size_ofp size_const T constr)
           (fn _ => simp_tac simpset 1))) constrs)
         (descr' ~~ size_fns ~~ recTs1);