src/Pure/Isar/class_declaration.ML

           (case eq_morph of
             SOME eq_morph => const_morph $> eq_morph
           | NONE => const_morph);
         val thm'' = Morphism.thm const_eq_morph thm';
         val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
-      in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
+      in Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'') (K tac) end;
     val assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
 
     (* of_class *)
     val of_class_prop_concl = Logic.mk_of_class (aT, class);
     val of_class_prop =

     val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
     val tac =
       REPEAT (SOMEGOAL
         (Tactic.match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
           ORELSE' Tactic.assume_tac));
-    val of_class = Skip_Proof.prove_global thy [] [] of_class_prop (K tac);
+    val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (K tac);
 
   in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end;
 
 
 (* reading and processing class specifications *)