# HG changeset patch
# User haftmann
# Date 1237751172 -3600
# Node ID db260dfd2d8c3ebaaf9e96cc5ad5347f5573b275
# Parent  ddb1fafa2dcbbd67084dc9059e86e2637581e798
more antiquotations

diff -r ddb1fafa2dcb -r db260dfd2d8c src/HOL/Tools/Qelim/qelim.ML
--- 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)