changeset 8438 | b8389b4fca9c |
parent 6970 | ac37a8fcaad1 |
child 12109 | bd6eb9194a5d |
--- a/src/ZF/Tools/induct_tacs.ML Mon Mar 13 13:27:44 2000 +0100 +++ b/src/ZF/Tools/induct_tacs.ML Mon Mar 13 13:28:31 2000 +0100 @@ -175,7 +175,7 @@ in thy |> Theory.add_path (Sign.base_name big_rec_name) - |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])] + |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]) |> DatatypesData.put (Symtab.update ((big_rec_name, dt_info), DatatypesData.get thy))