src/HOL/Library/positivstellensatz.ML
changeset 59586 ddf6deaadfe8
parent 59582 0fbed69ff081
child 60642 48dd1cefb4ae
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Mar 04 20:50:20 2015 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Mar 04 22:05:01 2015 +0100
     1.3 @@ -515,20 +515,20 @@
     1.4  
     1.5      fun mk_forall x th =
     1.6        Drule.arg_cong_rule
     1.7 -        (instantiate_cterm' [SOME (Thm.ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" })
     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  
    1.11      val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
    1.12  
    1.13      fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
    1.14 -    fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_term v)) (Thm.lambda v t)
    1.15 +    fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
    1.16  
    1.17      fun choose v th th' =
    1.18        case Thm.concl_of th of
    1.19          @{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
    1.20          let
    1.21            val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
    1.22 -          val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_term) p
    1.23 +          val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
    1.24            val th0 = fconv_rule (Thm.beta_conversion true)
    1.25              (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
    1.26            val pv = (Thm.rhs_of o Thm.beta_conversion true)