# HG changeset patch
# User paulson
# Date 1115649611 -7200
# Node ID 08e8d3fb93438ae1a6dd487e648e8dacece8ef3f
# Parent  9b00875e21f7c650ba6f4f2efa2de9ec5ab634c4
choice_const moved to hologic.ML

diff -r 9b00875e21f7 -r 08e8d3fb9343 src/HOL/Tools/specification_package.ML
--- 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
diff -r 9b00875e21f7 -r 08e8d3fb9343 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Mon May 09 16:38:56 2005 +0200
+++ b/src/HOL/hologic.ML	Mon May 09 16:40:11 2005 +0200
@@ -27,12 +27,14 @@
   val mk_disj: term * term -> term
   val mk_imp: term * term -> term
   val dest_conj: term -> term list
+  val dest_disj: term -> term list
   val dest_imp: term -> term * term
   val dest_not: term -> term
   val dest_concls: term -> term list
   val eq_const: typ -> term
   val all_const: typ -> term
   val exists_const: typ -> term
+  val choice_const: typ -> term
   val Collect_const: typ -> term
   val mk_eq: term * term -> term
   val dest_eq: term -> term * term
@@ -137,6 +139,9 @@
 fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
   | dest_conj t = [t];
 
+fun dest_disj (Const ("op |", _) $ t $ t') = t :: dest_disj t'
+  | dest_disj t = [t];
+
 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
   | dest_imp  t = raise TERM ("dest_imp", [t]);
 
@@ -159,6 +164,8 @@
 fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
 fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
 
+fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T)
+
 fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T);
 fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);