--- a/quotient.ML	Tue Nov 24 19:09:29 2009 +0100
+++ b/quotient.ML	Wed Nov 25 03:45:44 2009 +0100
@@ -1,5 +1,7 @@
 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
 
@@ -9,6 +11,8 @@
 structure Quotient: QUOTIENT =
 struct
 
+exception LIFT_MATCH of string
+
 (* wrappers for define, note and theorem_i *)
 fun define (name, mx, rhs) lthy =
 let