--- a/Attic/Quot/quotient_tacs.ML	Mon Mar 15 17:51:35 2010 +0100
+++ b/Attic/Quot/quotient_tacs.ML	Mon Mar 15 17:52:31 2010 +0100
@@ -603,9 +603,9 @@
   val rtrm' = HOLogic.dest_Trueprop rtrm
   val qtrm' = HOLogic.dest_Trueprop qtrm
   val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
-    handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
+    handle (ERROR msg) => lift_match_error ctxt msg rtrm qtrm
   val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
-    handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
+    handle (ERROR msg) => lift_match_error ctxt msg rtrm qtrm
 in
   Drule.instantiate' []
     [SOME (cterm_of thy rtrm'),

--- a/Attic/Quot/quotient_term.ML	Mon Mar 15 17:51:35 2010 +0100
+++ b/Attic/Quot/quotient_term.ML	Mon Mar 15 17:52:31 2010 +0100
@@ -7,8 +7,6 @@
 
 signature QUOTIENT_TERM =
 sig
-  exception LIFT_MATCH of string
-
   datatype flag = AbsF | RepF
 
   val absrep_fun: flag -> Proof.context -> typ * typ -> term
@@ -65,7 +63,7 @@
 fun get_mapfun ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
-  val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
+  val exn = error ("No map function for type " ^ quote s ^ " found.")
   val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
 in
   Const (mapfun, dummyT)
@@ -91,7 +89,7 @@
       TVar _ => mk_Free rty
     | Type (_, []) => mk_identity rty
     | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
-    | _ => raise LIFT_MATCH "mk_mapfun (default)"
+    | _ => raise (error "mk_mapfun (default)")
 in
   fold_rev Term.lambda vs' (mk_mapfun_aux rty)
 end
@@ -102,7 +100,7 @@
 fun get_rty_qty ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
-  val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
+  val exn = error ("No quotient type " ^ quote s ^ " found.")
   val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
 in
   (#rtyp qdata, #qtyp qdata)
@@ -148,7 +146,7 @@
   val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   val ty_str = Syntax.string_of_typ ctxt ty
 in
-  raise LIFT_MATCH (space_implode " "
+  raise error (cat_lines
     ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
 end
 
@@ -233,9 +231,9 @@
     | (TFree x, TFree x') =>
         if x = x'
         then mk_identity rty
-        else raise (LIFT_MATCH "absrep_fun (frees)")
+        else raise (error "absrep_fun (frees)")
     | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
-    | _ => raise (LIFT_MATCH "absrep_fun (default)")
+    | _ => raise (error "absrep_fun (default)")
 
 fun absrep_fun_chk flag ctxt (rty, qty) =
   absrep_fun flag ctxt (rty, qty)
@@ -270,7 +268,7 @@
 fun get_relmap ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
-  val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
+  val exn = error ("get_relmap (no relation map function found for type " ^ s ^ ")")
   val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
 in
   Const (relmap, dummyT)
@@ -285,7 +283,7 @@
       TVar _ => mk_Free rty
     | Type (_, []) => HOLogic.eq_const rty
     | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
-    | _ => raise LIFT_MATCH ("mk_relmap (default)")
+    | _ => raise (error "mk_relmap (default)")
 in
   fold_rev Term.lambda vs' (mk_relmap_aux rty)
 end
@@ -293,7 +291,7 @@
 fun get_equiv_rel ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
-  val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
+  val exn = error ("get_quotdata (no quotient found for type " ^ s ^ ")")
 in
   #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
 end
@@ -303,7 +301,7 @@
   val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   val ty_str = Syntax.string_of_typ ctxt ty
 in
-  raise LIFT_MATCH (space_implode " "
+  raise error (space_implode " "
     ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
 end
 
@@ -410,7 +408,7 @@
   val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
   val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
 in
-  raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
+  raise error (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
 end
 
 (* the major type of All and Ex quantifiers *)
@@ -573,14 +571,14 @@
 
   | (Bound i, Bound i') =>
        if i = i' then rtrm
-       else raise (LIFT_MATCH "regularize (bounds mismatch)")
+       else raise (error "regularize (bounds mismatch)")
 
   | _ =>
        let
          val rtrm_str = Syntax.string_of_term ctxt rtrm
          val qtrm_str = Syntax.string_of_term ctxt qtrm
        in
-         raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
+         raise (error ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
        end
 
 fun regularize_trm_chk ctxt (rtrm, qtrm) =
@@ -628,7 +626,7 @@
   val rtrm_str = Syntax.string_of_term ctxt rtrm
   val qtrm_str = Syntax.string_of_term ctxt qtrm
 in
-  raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
+  raise error (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
 end