--- a/src/HOL/Tools/semiring_normalizer.ML Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Mon Jun 01 18:59:21 2015 +0200
@@ -127,12 +127,12 @@
let
fun numeral_is_const ct =
case Thm.term_of ct of
- Const (@{const_name Fields.divide},_) $ a $ b =>
+ Const (@{const_name Rings.divide},_) $ a $ b =>
can HOLogic.dest_number a andalso can HOLogic.dest_number b
| Const (@{const_name Fields.inverse},_)$t => can HOLogic.dest_number t
| t => can HOLogic.dest_number t
fun dest_const ct = ((case Thm.term_of ct of
- Const (@{const_name Fields.divide},_) $ a $ b=>
+ Const (@{const_name Rings.divide},_) $ a $ b=>
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
| Const (@{const_name Fields.inverse},_)$t =>
Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))