--- a/src/ZF/Tools/induct_tacs.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Sat Jan 21 23:02:14 2006 +0100
@@ -165,7 +165,7 @@
in
thy
|> Theory.add_path (Sign.base_name big_rec_name)
- |> PureThy.add_thmss [(("simps", simps), [Attrib.theory Simplifier.simp_add])] |> snd
+ |> PureThy.add_thmss [(("simps", simps), [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