src/HOL/Tools/groebner.ML

--- a/src/HOL/Tools/groebner.ML	Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/groebner.ML	Thu Aug 19 11:02:14 2010 +0200
@@ -395,7 +395,7 @@
 
 fun refute_disj rfn tm =
  case term_of tm of
-  Const("op |",_)$l$r =>
+  Const(@{const_name "op |"},_)$l$r =>
    compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE))
   | _ => rfn tm ;
 
@@ -405,11 +405,11 @@
 val mk_comb = capply;
 fun is_neg t =
     case term_of t of
-      (Const("Not",_)$p) => true
+      (Const(@{const_name "Not"},_)$p) => true
     | _  => false;
 fun is_eq t =
  case term_of t of
- (Const("op =",_)$_$_) => true
+ (Const(@{const_name "op ="},_)$_$_) => true
 | _  => false;
 
 fun end_itlist f l =
@@ -430,14 +430,14 @@
 val strip_exists =
  let fun h (acc, t) =
       case (term_of t) of
-       Const("Ex",_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
+       Const(@{const_name "Ex"},_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
      | _ => (acc,t)
  in fn t => h ([],t)
  end;
 
 fun is_forall t =
  case term_of t of
-  (Const("All",_)$Abs(_,_,_)) => true
+  (Const(@{const_name "All"},_)$Abs(_,_,_)) => true
 | _ => false;
 
 val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
@@ -522,7 +522,7 @@
  fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
 
 fun choose v th th' = case concl_of th of 
-  @{term Trueprop} $ (Const("Ex",_)$_) => 
+  @{term Trueprop} $ (Const(@{const_name "Ex"},_)$_) => 
    let
     val p = (funpow 2 Thm.dest_arg o cprop_of) th
     val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
@@ -923,15 +923,15 @@
 
 fun find_term bounds tm =
   (case term_of tm of
-    Const ("op =", T) $ _ $ _ =>
+    Const (@{const_name "op ="}, T) $ _ $ _ =>
       if domain_type T = HOLogic.boolT then find_args bounds tm
       else dest_arg tm
-  | Const ("Not", _) $ _ => find_term bounds (dest_arg tm)
-  | Const ("All", _) $ _ => find_body bounds (dest_arg tm)
-  | Const ("Ex", _) $ _ => find_body bounds (dest_arg tm)
-  | Const ("op &", _) $ _ $ _ => find_args bounds tm
-  | Const ("op |", _) $ _ $ _ => find_args bounds tm
-  | Const ("op -->", _) $ _ $ _ => find_args bounds tm
+  | Const (@{const_name "Not"}, _) $ _ => find_term bounds (dest_arg tm)
+  | Const (@{const_name "All"}, _) $ _ => find_body bounds (dest_arg tm)
+  | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (dest_arg tm)
+  | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
+  | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+  | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
   | @{term "op ==>"} $_$_ => find_args bounds tm
   | Const("op ==",_)$_$_ => find_args bounds tm
   | @{term Trueprop}$_ => find_term bounds (dest_arg tm)
@@ -985,7 +985,7 @@
 
 local
  fun lhs t = case term_of t of
-  Const("op =",_)$_$_ => Thm.dest_arg1 t
+  Const(@{const_name "op ="},_)$_$_ => Thm.dest_arg1 t
  | _=> raise CTERM ("ideal_tac - lhs",[t])
  fun exitac NONE = no_tac
    | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1