changeset 6092 | d9db67970c73 |
parent 6070 | 032babd0120b |
child 6112 | 5e4871c5136b |
--- a/src/ZF/Tools/induct_tacs.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/ZF/Tools/induct_tacs.ML Tue Jan 12 13:54:51 1999 +0100 @@ -165,8 +165,7 @@ in thy |> Theory.add_path (Sign.base_name big_rec_name) - |> PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), - [Simplifier.simp_add_global])] + |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])] |> DatatypesData.put (Symtab.update ((big_rec_name, dt_info), DatatypesData.get thy))