src/HOL/Tools/typedef.ML

             val cert = Thm.cterm_of (Thm.theory_of_thm def_eq);
             val goal_eq = MetaSimplifier.rewrite true [def_eq] (cert goal');
           in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
 
     fun typedef_result inhabited =
-      ObjectLogic.typedecl (tname, vs, mx)
+      Object_Logic.typedecl (tname, vs, mx)
       #> snd
       #> Sign.add_consts_i
         [(Rep_name, newT --> oldT, NoSyn),
          (Abs_name, oldT --> newT, NoSyn)]
       #> add_def