src/ZF/Tools/induct_tacs.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 15703 727ef1b8b3ee
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -178,7 +178,7 @@
     1.4                (Symtab.update
     1.5                 ((big_rec_name, dt_info), DatatypesData.get thy))
     1.6            |> ConstructorsData.put
     1.7 -               (Library.foldr Symtab.update (con_pairs, ConstructorsData.get thy))
     1.8 +               (foldr Symtab.update (ConstructorsData.get thy) con_pairs)
     1.9            |> Theory.parent_path
    1.10    end;
    1.11