src/HOL/Boogie/Tools/boogie_loader.ML

       (case lookup_type_name thy isa_name arity of
         SOME type_name => (((name, type_name), log_ex name type_name), thy)
       | NONE =>
           let
             val args = Name.variant_list [] (replicate arity "'")
-            val (T, thy') = ObjectLogic.typedecl (Binding.name isa_name, args,
-              mk_syntax name arity) thy
+            val (T, thy') =
+              Object_Logic.typedecl (Binding.name isa_name, args, mk_syntax name arity) thy
             val type_name = fst (Term.dest_Type T)
           in (((name, type_name), log_new name type_name), thy') end)
     end
 in
 fun declare_types verbose tys =