src/ZF/Tools/induct_tacs.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 21350 6e58289b6685
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sat Jan 21 23:02:14 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), [Attrib.theory Simplifier.simp_add])] |> snd
     1.8 +    |> PureThy.add_thmss [(("simps", simps), [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