# HG changeset patch
# User chaieb
# Date 1238955711 -3600
# Node ID 1040425c86a22a16f4e34015ece8992fb7fd4073
# Parent  6fff6030338b3f73039088169b962f6d0beb295c
fixed usage of rational constants

diff -r 6fff6030338b -r 1040425c86a2 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- 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 =
diff -r 6fff6030338b -r 1040425c86a2 src/HOL/Library/normarith.ML
--- a/src/HOL/Library/normarith.ML	Sun Apr 05 19:21:51 2009 +0100
+++ b/src/HOL/Library/normarith.ML	Sun Apr 05 19:21:51 2009 +0100
@@ -369,6 +369,7 @@
 
   fun dest_ratconst t = case term_of t of
    Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
+ | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
  | _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
  fun is_ratconst t = can dest_ratconst t
 
@@ -795,8 +796,9 @@
 
  open Conv Thm Conv2;
  val bool_eq = op = : bool *bool -> bool
- fun dest_ratconst t = case term_of t of
+  fun dest_ratconst t = case term_of t of
    Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
+ | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
  | _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
  fun is_ratconst t = can dest_ratconst t
  fun augment_norm b t acc = case term_of t of