src/HOL/Tools/specification_package.ML
changeset 15945 08e8d3fb9343
parent 15794 5de27a5fc5ed
child 17057 0934ac31985f
--- a/src/HOL/Tools/specification_package.ML	Mon May 09 16:38:56 2005 +0200
+++ b/src/HOL/Tools/specification_package.ML	Mon May 09 16:40:11 2005 +0200
@@ -29,9 +29,6 @@
 val helper = Goals.result()
 end
 
-(* Akin to HOLogic.exists_const *)
-fun choice_const T = Const("Hilbert_Choice.Eps",(T-->HOLogic.boolT)-->T)
-
 (* Actual code *)
 
 local
@@ -45,7 +42,8 @@
 		val cdefname = if thname = ""
 			       then Thm.def_name (Sign.base_name cname)
 			       else thname
-		val def_eq = Logic.mk_equals (Const(cname_full,ctype),choice_const ctype $  P)
+		val def_eq = Logic.mk_equals (Const(cname_full,ctype),
+		                              HOLogic.choice_const ctype $  P)
 		val (thy',thms) = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy
 		val thm' = [thm,hd thms] MRS helper
 	    in