1.1 --- a/src/HOL/Tools/groebner.ML	Thu Aug 19 16:08:54 2010 +0200
     1.2 +++ b/src/HOL/Tools/groebner.ML	Thu Aug 19 16:08:59 2010 +0200
     1.3 @@ -405,7 +405,7 @@
     1.4  val mk_comb = capply;
     1.5  fun is_neg t =
     1.6      case term_of t of
     1.7 -      (Const(@{const_name "Not"},_)$p) => true
     1.8 +      (Const(@{const_name Not},_)$p) => true
     1.9      | _  => false;
    1.10  fun is_eq t =
    1.11   case term_of t of
    1.12 @@ -430,14 +430,14 @@
    1.13  val strip_exists =
    1.14   let fun h (acc, t) =
    1.15        case (term_of t) of
    1.16 -       Const(@{const_name "Ex"},_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
    1.17 +       Const(@{const_name Ex},_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
    1.18       | _ => (acc,t)
    1.19   in fn t => h ([],t)
    1.20   end;
    1.21  
    1.22  fun is_forall t =
    1.23   case term_of t of
    1.24 -  (Const(@{const_name "All"},_)$Abs(_,_,_)) => true
    1.25 +  (Const(@{const_name All},_)$Abs(_,_,_)) => true
    1.26  | _ => false;
    1.27  
    1.28  val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
    1.29 @@ -522,7 +522,7 @@
    1.30   fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
    1.31  
    1.32  fun choose v th th' = case concl_of th of 
    1.33 -  @{term Trueprop} $ (Const(@{const_name "Ex"},_)$_) => 
    1.34 +  @{term Trueprop} $ (Const(@{const_name Ex},_)$_) => 
    1.35     let
    1.36      val p = (funpow 2 Thm.dest_arg o cprop_of) th
    1.37      val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
    1.38 @@ -926,9 +926,9 @@
    1.39      Const (@{const_name "op ="}, T) $ _ $ _ =>
    1.40        if domain_type T = HOLogic.boolT then find_args bounds tm
    1.41        else dest_arg tm
    1.42 -  | Const (@{const_name "Not"}, _) $ _ => find_term bounds (dest_arg tm)
    1.43 -  | Const (@{const_name "All"}, _) $ _ => find_body bounds (dest_arg tm)
    1.44 -  | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (dest_arg tm)
    1.45 +  | Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm)
    1.46 +  | Const (@{const_name All}, _) $ _ => find_body bounds (dest_arg tm)
    1.47 +  | Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
    1.48    | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
    1.49    | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
    1.50    | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm