src/ZF/Tools/induct_tacs.ML

           |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
           |> DatatypesData.put
               (Symtab.update
                ((big_rec_name, dt_info), DatatypesData.get thy))
           |> ConstructorsData.put
-               (Library.foldr Symtab.update (con_pairs, ConstructorsData.get thy))
+               (foldr Symtab.update (ConstructorsData.get thy) con_pairs)
           |> Theory.parent_path
   end;
 
 fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
   let