# HG changeset patch
# User nipkow
# Date 1181571663 -7200
# Node ID 71e99443e17d30c03ad351622a226a1d8113a44b
# Parent  156db04f8af0bbf169e0d1737a946a155e6f1357
hid constant "dom"

diff -r 156db04f8af0 -r 71e99443e17d src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Mon Jun 11 11:10:04 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Mon Jun 11 16:21:03 2007 +0200
@@ -125,6 +125,7 @@
 class ring_no_zero_divisors = ring + no_zero_divisors
 
 class dom = ring_1 + ring_no_zero_divisors
+hide const dom
 
 class idom = comm_ring_1 + no_zero_divisors