--- a/src/HOL/Tools/choice_specification.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML Thu Aug 19 16:08:59 2010 +0200
@@ -24,7 +24,7 @@
fun mk_definitional [] arg = arg
| mk_definitional ((thname,cname,covld)::cos) (thy,thm) =
case HOLogic.dest_Trueprop (concl_of thm) of
- Const(@{const_name "Ex"},_) $ P =>
+ Const(@{const_name Ex},_) $ P =>
let
val ctype = domain_type (type_of P)
val cname_full = Sign.intern_const thy cname
@@ -51,7 +51,7 @@
end
| process ((thname,cname,covld)::cos) (thy,tm) =
case tm of
- Const(@{const_name "Ex"},_) $ P =>
+ Const(@{const_name Ex},_) $ P =>
let
val ctype = domain_type (type_of P)
val cname_full = Sign.intern_const thy cname