--- a/quotient.ML	Fri Nov 20 13:03:01 2009 +0100
+++ b/quotient.ML	Sat Nov 21 02:49:39 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,9 @@
 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
@@ -150,15 +155,17 @@
   val _ = tracing ("storing under: " ^ qty_str)
   val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2  
   (* FIXME: varifyT should not be used *)
+  (* storing of the equiv_thm under a name *)
+  val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm) lthy3
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
-  val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3;
+  val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4;
   val eqn1i = Thm.prop_of (symmetric eqn1pre)
-  val ((_, [eqn2pre]), lthy5) = Variable.import true [REP_def] lthy4;
+  val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5;
   val eqn2i = Thm.prop_of (symmetric eqn2pre)
 
-  val exp_morphism = ProofContext.export_morphism lthy5 (ProofContext.init (ProofContext.theory_of lthy5));
+  val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6));
   val exp_term = Morphism.term exp_morphism;
   val exp = Morphism.thm exp_morphism;
 
@@ -169,14 +176,14 @@
   val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
     Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]
 in
-  lthy5
+  lthy6
   |> note (quot_thm_name, quot_thm)
   ||>> note (quotient_thm_name, quotient_thm)
   ||> Local_Theory.theory (fn thy =>
       let
         val global_eqns = map exp_term [eqn2i, eqn1i];
         (* Not sure if the following context should not be used *)
-        val (global_eqns2, lthy6) = Variable.import_terms true global_eqns lthy5;
+        val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6;
         val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
       in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
 end