# HG changeset patch
# User wenzelm
# Date 1082053850 -7200
# Node ID 0bf4e84bf51d09c5e283b3eab96d0b319eb697a6
# Parent  78b75a9eec010f8ba875055694e56c6b8ba5e80e
finalconsts RepC AbsC;

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