src/HOL/Tools/Nitpick/nitpick_hol.ML

       partition_axioms_by_definitionality ctxt user_axioms def_names
     val (built_in_nondefs, user_nondefs) =
       List.partition (is_typedef_axiom ctxt false) user_nondefs
       |>> append built_in_nondefs
     val defs =
-      (thy |> PureThy.all_thms_of
+      (thy |> Global_Theory.all_thms_of
            |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
            |> map (prop_of o snd)
            |> filter_out is_trivial_definition
            |> filter is_plain_definition) @
       user_defs @ built_in_defs

   end
 
 fun ground_theorem_table thy =
   fold ((fn @{const Trueprop} $ t1 =>
             is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
-          | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty
+          | _ => I) o prop_of o snd) (Global_Theory.all_thms_of thy) Inttab.empty
 
 (* TODO: Move to "Nitpick.thy" *)
 val basic_ersatz_table =
   [(@{const_name card}, @{const_name card'}),
    (@{const_name setsum}, @{const_name setsum'}),