# HG changeset patch
# User nipkow
# Date 1256829837 -3600
# Node ID 2b5b0f9e271c7db2d72bd64aa236f328f099201f
# Parent  1932908057c71aad640aad9cde935f894cc2d950
Replaced exception CRing by error because it is meant for the user.

diff -r 1932908057c7 -r 2b5b0f9e271c src/HOL/Library/comm_ring.ML
--- a/src/HOL/Library/comm_ring.ML	Thu Oct 29 15:47:03 2009 +0100
+++ b/src/HOL/Library/comm_ring.ML	Thu Oct 29 16:23:57 2009 +0100
@@ -12,9 +12,6 @@
 structure CommRing: COMM_RING =
 struct
 
-(* The Cring exception for erronous uses of cring_tac *)
-exception CRing of string;
-
 (* Zero and One of the commutative ring *)
 fun cring_zero T = Const (@{const_name HOL.zero}, T);
 fun cring_one T = Const (@{const_name HOL.one}, T);
@@ -76,8 +73,8 @@
           val crhs = cterm_of thy (reif_polex T fs rhs);
           val ca = ctyp_of thy T;
         in (ca, cvs, clhs, crhs) end
-      else raise CRing ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
-  | reif_eq _ _ = raise CRing "reif_eq: not an equation";
+      else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
+  | reif_eq _ _ = error "reif_eq: not an equation";
 
 (* The cring tactic *)
 (* Attention: You have to make sure that no t^0 is in the goal!! *)