--- 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,