--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue May 31 23:06:03 2016 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Jun 01 10:45:35 2016 +0200
@@ -897,9 +897,9 @@
fun dest_frac ct =
case Thm.term_of ct of
Const (@{const_name Rings.divide},_) $ a $ b=>
- Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
- | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
- | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
+ Rat.make (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
+ | Const(@{const_name inverse}, _)$a => Rat.make(1, HOLogic.dest_number a |> snd)
+ | t => Rat.of_int (snd (HOLogic.dest_number t))
fun whatis x ct = case Thm.term_of ct of
Const(@{const_name Groups.plus}, _)$(Const(@{const_name Groups.times},_)$_$y)$_ =>