--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Apr 05 19:21:51 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Apr 05 19:21:51 2009 +0100
@@ -657,6 +657,7 @@
fun dest_frac ct = case term_of ct of
Const (@{const_name "HOL.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))
fun mk_frac phi cT x =