src/ZF/Tools/induct_tacs.ML

     val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
 
   in
     thy
     |> Theory.add_path (Sign.base_name big_rec_name)
-    |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])] |> snd
+    |> PureThy.add_thmss [(("simps", simps), [Attrib.theory Simplifier.simp_add])] |> snd
     |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
     |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
     |> Theory.parent_path
   end;