diff -r 1e61f23fd359 -r 0ee05eef881b src/HOL/Tools/specification_package.ML
--- 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