# HG changeset patch
# User chaieb
# Date 1192962792 -7200
# Node ID 962e4f4142fade1ff24b3cab28a79428cc59bc04
# Parent  afb5e602ce9d9036ccb0124b4e50b8a4050df444
Fixed Bug in instantiation of Groebner Bases to field: dest_const used to raise TERM where the tactic handles ERROR

diff -r afb5e602ce9d -r 962e4f4142fa src/HOL/Arith_Tools.thy
--- a/src/HOL/Arith_Tools.thy	Sun Oct 21 02:49:16 2007 +0200
+++ b/src/HOL/Arith_Tools.thy	Sun Oct 21 12:33:12 2007 +0200
@@ -584,10 +584,11 @@
  | Const (@{const_name "HOL.uminus"},_)$t => numeral_is_const (Thm.dest_arg ct)
  | t => can HOLogic.dest_number t
 
-fun dest_const ct = case term_of ct of
+fun dest_const 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))
- | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
+ | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
+   handle TERM _ => error "ring_dest_const")
 
 fun mk_const phi cT x =
  let val (a, b) = Rat.quotient_of_rat x