src/ZF/Tools/induct_tacs.ML
changeset 18688 abf0f018b5ec
parent 18418 bf448d999b7e
child 18708 4b3dadb4fe33
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Sat Jan 14 17:20:51 2006 +0100
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sat Jan 14 22:25:34 2006 +0100
     1.3 @@ -165,7 +165,7 @@
     1.4    in
     1.5      thy
     1.6      |> Theory.add_path (Sign.base_name big_rec_name)
     1.7 -    |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])] |> snd
     1.8 +    |> PureThy.add_thmss [(("simps", simps), [Attrib.theory Simplifier.simp_add])] |> snd
     1.9      |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
    1.10      |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
    1.11      |> Theory.parent_path