src/HOL/Library/positivstellensatz.ML
changeset 60949 ccbf9379e355
parent 60801 7664e0916eec
child 61075 f6b0d827240e
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Sun Aug 16 18:19:30 2015 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Sun Aug 16 19:25:08 2015 +0200
     1.3 @@ -540,7 +540,7 @@
     1.4      fun simple_choose v th =
     1.5        choose v
     1.6          (Thm.assume
     1.7 -          ((Thm.apply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
     1.8 +          ((Thm.apply @{cterm Trueprop} o mk_ex v) (Thm.dest_arg (hd (Thm.chyps_of th))))) th
     1.9  
    1.10      val strip_forall =
    1.11        let