src/ZF/Tools/datatype_package.ML
changeset 18377 0e1d025d57b3
parent 18358 0a733e11021a
child 18418 bf448d999b7e
     1.1 --- a/src/ZF/Tools/datatype_package.ML	Thu Dec 08 20:16:17 2005 +0100
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Fri Dec 09 09:06:45 2005 +0100
     1.3 @@ -366,14 +366,14 @@
     1.4   in
     1.5    (*Updating theory components: simprules and datatype info*)
     1.6    (thy1 |> Theory.add_path big_rec_base_name
     1.7 -        |> (#1 o PureThy.add_thmss
     1.8 +        |> PureThy.add_thmss
     1.9           [(("simps", simps), [Simplifier.simp_add_global]),
    1.10            (("", intrs), [Classical.safe_intro_global]),
    1.11            (("con_defs", con_defs), []),
    1.12            (("case_eqns", case_eqns), []),
    1.13            (("recursor_eqns", recursor_eqns), []),
    1.14            (("free_iffs", free_iffs), []),
    1.15 -          (("free_elims", free_SEs), [])])
    1.16 +          (("free_elims", free_SEs), [])] |> snd
    1.17          |> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
    1.18          |> ConstructorsData.map (fold Symtab.update con_pairs)
    1.19          |> Theory.parent_path,