src/HOL/Library/positivstellensatz.ML
changeset 38549 d0385f2764d8
parent 37598 893dcabf0c04
child 38558 32ad17fe2b9c
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Aug 19 10:27:12 2010 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Aug 19 11:02:14 2010 +0200
     1.3 @@ -498,7 +498,7 @@
     1.4   val strip_exists =
     1.5    let fun h (acc, t) =
     1.6     case (term_of t) of
     1.7 -    Const("Ex",_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
     1.8 +    Const(@{const_name "Ex"},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
     1.9    | _ => (acc,t)
    1.10    in fn t => h ([],t)
    1.11    end
    1.12 @@ -515,7 +515,7 @@
    1.13   fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
    1.14  
    1.15   fun choose v th th' = case concl_of th of 
    1.16 -   @{term Trueprop} $ (Const("Ex",_)$_) => 
    1.17 +   @{term Trueprop} $ (Const(@{const_name "Ex"},_)$_) => 
    1.18      let
    1.19       val p = (funpow 2 Thm.dest_arg o cprop_of) th
    1.20       val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
    1.21 @@ -533,7 +533,7 @@
    1.22   val strip_forall =
    1.23    let fun h (acc, t) =
    1.24     case (term_of t) of
    1.25 -    Const("All",_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
    1.26 +    Const(@{const_name "All"},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
    1.27    | _ => (acc,t)
    1.28    in fn t => h ([],t)
    1.29    end