src/ZF/Tools/datatype_package.ML

   (* Build the new theory *)
 
   val need_recursor = (not coind andalso recursor_typ <> case_typ);
 
   fun add_recursor thy =
-      if need_recursor then
-           thy |> Sign.add_consts_i
-                    [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
-               |> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
-      else thy;
+    if need_recursor then
+      thy
+      |> Sign.add_consts_i
+        [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
+      |> (snd o Global_Theory.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
+    else thy;
 
   val (con_defs, thy0) = thy_path
              |> Sign.add_consts_i
                  (map (fn (c, T, mx) => (Binding.name c, T, mx))
                   ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists)))
-             |> PureThy.add_defs false
+             |> Global_Theory.add_defs false
                  (map (Thm.no_attributes o apfst Binding.name)
                   (case_def ::
                    flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists))))
              ||> add_recursor
              ||> Sign.parent_path

   val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
 
  in
   (*Updating theory components: simprules and datatype info*)
   (thy1 |> Sign.add_path big_rec_base_name
-        |> PureThy.add_thmss
+        |> Global_Theory.add_thmss
          [((Binding.name "simps", simps), [Simplifier.simp_add]),
           ((Binding.empty , intrs), [Classical.safe_intro NONE]),
           ((Binding.name "con_defs", con_defs), []),
           ((Binding.name "case_eqns", case_eqns), []),
           ((Binding.name "recursor_eqns", recursor_eqns), []),