src/HOLCF/Tools/Domain/domain_extender.ML

                 Domain_Theorems.theorems (eq, eqs) dbind cs info take_info)
              (dbinds ~~ eqs ~~ eqs' ~~ iso_infos)
           ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
   in
     theorems_thy
-      |> PureThy.add_thmss
+      |> Global_Theory.add_thmss
            [((Binding.qualified true "rews" comp_dbind,
               flat rewss @ take_rews), [])]
       |> snd
   end;