--- a/src/HOL/Tools/specification_package.ML Wed Oct 08 16:02:54 2003 +0200
+++ b/src/HOL/Tools/specification_package.ML Thu Oct 09 18:13:32 2003 +0200
@@ -72,9 +72,7 @@
then Thm.def_name (Sign.base_name cname)
else thname
val co = Const(cname_full,ctype)
- val def = Logic.mk_implies(HOLogic.mk_Trueprop HOLogic.false_const,
- Logic.mk_equals (co,choice_const ctype $ P))
- val (thy',_) = PureThy.add_defs_i covld [((cdefname,def),[])] thy
+ val thy' = Theory.add_finals_i covld [co] thy
val tm' = case P of
Abs(_, _, bodt) => subst_bound (co, bodt)
| _ => P $ co