src/HOL/Library/positivstellensatz.ML
changeset 61075 f6b0d827240e
parent 60949 ccbf9379e355
child 61609 77b453bd616f
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Aug 31 22:45:40 2015 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Tue Sep 01 17:25:36 2015 +0200
     1.3 @@ -514,14 +514,15 @@
     1.4        | _ => "x"
     1.5  
     1.6      fun mk_forall x th =
     1.7 -      Drule.arg_cong_rule
     1.8 -        (instantiate_cterm' [SOME (Thm.ctyp_of_cterm x)] [] @{cpat "All :: (?'a => bool) => _" })
     1.9 -        (Thm.abstract_rule (name_of x) x th)
    1.10 +      let
    1.11 +        val T = Thm.typ_of_cterm x
    1.12 +        val all = Thm.cterm_of ctxt (Const (@{const_name All}, (T --> @{typ bool}) --> @{typ bool}))
    1.13 +      in Drule.arg_cong_rule all (Thm.abstract_rule (name_of x) x th) end
    1.14  
    1.15      val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec));
    1.16  
    1.17 -    fun ext T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat Ex}
    1.18 -    fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
    1.19 +    fun ext T = Thm.cterm_of ctxt (Const (@{const_name Ex}, (T --> @{typ bool}) --> @{typ bool}))
    1.20 +    fun mk_ex v t = Thm.apply (ext (Thm.typ_of_cterm v)) (Thm.lambda v t)
    1.21  
    1.22      fun choose v th th' =
    1.23        case Thm.concl_of th of