src/HOL/Library/positivstellensatz.ML
changeset 63201 f151704c08e4
parent 63198 c583ca33076a
child 63205 97b721666890
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue May 31 23:06:03 2016 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 10:45:35 2016 +0200
     1.3 @@ -287,7 +287,7 @@
     1.4  
     1.5  fun cterm_of_rat x =
     1.6    let
     1.7 -    val (a, b) = Rat.quotient_of_rat x
     1.8 +    val (a, b) = Rat.dest x
     1.9    in
    1.10      if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
    1.11      else Thm.apply (Thm.apply @{cterm "op / :: real => _"}
    1.12 @@ -297,8 +297,8 @@
    1.13  
    1.14  fun dest_ratconst t =
    1.15    case Thm.term_of t of
    1.16 -    Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    1.17 -  | _ => Rat.rat_of_int (HOLogic.dest_number (Thm.term_of t) |> snd)
    1.18 +    Const(@{const_name divide}, _)$a$b => Rat.make(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    1.19 +  | _ => Rat.of_int (HOLogic.dest_number (Thm.term_of t) |> snd)
    1.20  fun is_ratconst t = can dest_ratconst t
    1.21  
    1.22  (*