1.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Apr 15 14:17:45 2004 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Apr 15 20:30:50 2004 +0200
     1.3 @@ -152,9 +152,10 @@
     1.4        |> (if def then (apsnd (Some o hd) oo (PureThy.add_defs_i false o map Thm.no_attributes))
     1.5             [Logic.mk_defpair (setC, set)]
     1.6            else rpair None)
     1.7 -      |>> PureThy.add_axioms_i [((typedef_name, typedef_prop),
     1.8 +      |>>> PureThy.add_axioms_i [((typedef_name, typedef_prop),
     1.9            [apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])]
    1.10 -      |> (fn ((theory', [type_definition]), set_def) =>
    1.11 +      |>> Theory.add_finals_i false [RepC, AbsC]
    1.12 +      |> (fn (theory', (set_def, [type_definition])) =>
    1.13          let
    1.14            fun make th = Drule.standard (th OF [type_definition]);
    1.15            val (theory'', [Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,