diff -r 0b60d8416ec5 -r 8237786171f1 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Fri Dec 25 00:17:55 2009 +0100
+++ b/Quot/quotient_typ.ML	Fri Dec 25 00:58:06 2009 +0100
@@ -1,9 +1,8 @@
 signature QUOTIENT_TYPE =
 sig
-  exception LIFT_MATCH of string
-
   val quotient_type: ((string list * binding * mixfix) * (typ * term)) list 
     -> Proof.context -> Proof.state
+
   val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list 
     -> Proof.context -> Proof.state
 end;
@@ -13,8 +12,6 @@
 
 open Quotient_Info;
 
-exception LIFT_MATCH of string
-
 (* wrappers for define, note, Attrib.internal and theorem_i *)
 fun define (name, mx, rhs) lthy =
 let
@@ -230,7 +227,7 @@
   fun after_qed thms lthy =
     fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd
 
-  (* sanity check*)  
+  (* sanity check *)  
   val _ = map sanity_check quot_list 
 in
   theorem after_qed goals lthy