1.1 --- a/src/HOL/Library/comm_ring.ML	Thu Oct 29 15:47:03 2009 +0100
     1.2 +++ b/src/HOL/Library/comm_ring.ML	Thu Oct 29 16:23:57 2009 +0100
     1.3 @@ -12,9 +12,6 @@
     1.4  structure CommRing: COMM_RING =
     1.5  struct
     1.6  
     1.7 -(* The Cring exception for erronous uses of cring_tac *)
     1.8 -exception CRing of string;
     1.9 -
    1.10  (* Zero and One of the commutative ring *)
    1.11  fun cring_zero T = Const (@{const_name HOL.zero}, T);
    1.12  fun cring_one T = Const (@{const_name HOL.one}, T);
    1.13 @@ -76,8 +73,8 @@
    1.14            val crhs = cterm_of thy (reif_polex T fs rhs);
    1.15            val ca = ctyp_of thy T;
    1.16          in (ca, cvs, clhs, crhs) end
    1.17 -      else raise CRing ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
    1.18 -  | reif_eq _ _ = raise CRing "reif_eq: not an equation";
    1.19 +      else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
    1.20 +  | reif_eq _ _ = error "reif_eq: not an equation";
    1.21  
    1.22  (* The cring tactic *)
    1.23  (* Attention: You have to make sure that no t^0 is in the goal!! *)