src/HOL/Library/positivstellensatz.ML

   end
  (* FIXME!!! Copied from groebner.ml *)
  val strip_exists =
   let fun h (acc, t) =
    case (term_of t) of
-    Const("Ex",_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+    Const(@{const_name "Ex"},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   | _ => (acc,t)
   in fn t => h ([],t)
   end
   fun name_of x = case term_of x of
    Free(s,_) => s

 
  fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
  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
      val th0 = fconv_rule (Thm.beta_conversion true)
          (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)

      choose v (Thm.assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
 
  val strip_forall =
   let fun h (acc, t) =
    case (term_of t) of
-    Const("All",_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+    Const(@{const_name "All"},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   | _ => (acc,t)
   in fn t => h ([],t)
   end
 
  fun f ct =