src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

             (list_comb (Const (name, T), args))))
         val lhs = Const (mode_cname, funT)
         val def = Logic.mk_equals (lhs, predterm)
         val ([definition], thy') = thy |>
           Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
-          PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
+          Global_Theory.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
         val ctxt' = ProofContext.init_global thy'
         val rules as ((intro, elim), _) =
           create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
         in thy'
           |> set_function_name Pred name mode mode_cname
           |> add_predfun_data name mode (definition, rules)
-          |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
-          |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
+          |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
+          |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
           |> Theory.checkpoint
         end;
   in
     thy |> defined_function_of Pred name |> fold create_definition modes
   end;

     val qname = #qname (dest_steps steps)
     val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
       (fn thm => Context.mapping (Code.add_eqn thm) I))))
     val thy''' =
       Output.cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ =>
-      fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
+      fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
       [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
         [attrib thy ])] thy))
       result_thms' thy'' |> Theory.checkpoint)
   in
     thy'''