--- a/quotient.ML	Tue Nov 24 15:15:33 2009 +0100
+++ b/quotient.ML	Tue Nov 24 15:31:29 2009 +0100
@@ -1,7 +1,5 @@
 signature QUOTIENT =
 sig
-  exception LIFT_MATCH of string 
-
   val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
   val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
 
@@ -11,9 +9,6 @@
 structure Quotient: QUOTIENT =
 struct
 
-(* exception for when quotient and lifted things do not match *)
-exception LIFT_MATCH of string 
-
 (* wrappers for define, note and theorem_i *)
 fun define (name, mx, rhs) lthy =
 let