--- a/src/HOL/Tools/Qelim/qelim.ML Sun Mar 22 20:46:12 2009 +0100
+++ b/src/HOL/Tools/Qelim/qelim.ML Sun Mar 22 20:46:12 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/Qelim/qelim.ML
- ID: $Id$
Author: Amine Chaieb, TU Muenchen
Generic quantifier elimination conversions for HOL formulae.
@@ -26,11 +25,12 @@
case (term_of p) of
Const(s,T)$_$_ =>
if domain_type T = HOLogic.boolT
- andalso s mem ["op &","op |","op -->","op ="]
+ andalso member (op =) [@{const_name "op &"}, @{const_name "op |"},
+ @{const_name "op -->"}, @{const_name "op ="}] s
then binop_conv (conv env) p
else atcv env p
- | Const("Not",_)$_ => arg_conv (conv env) p
- | Const("Ex",_)$Abs(s,_,_) =>
+ | Const(@{const_name "Not"},_)$_ => arg_conv (conv env) p
+ | Const(@{const_name "Ex"},_)$Abs(s,_,_) =>
let
val (e,p0) = Thm.dest_comb p
val (x,p') = Thm.dest_abs (SOME s) p0
@@ -41,8 +41,8 @@
val (l,r) = Thm.dest_equals (cprop_of th')
in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
else Thm.transitive (Thm.transitive th th') (conv env r) end
- | Const("Ex",_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
- | Const("All",_)$_ =>
+ | Const(@{const_name "Ex"},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
+ | Const(@{const_name "All"},_)$_ =>
let
val p = Thm.dest_arg p
val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)