--- a/FSet.thy	Thu Nov 12 12:07:33 2009 +0100
+++ b/FSet.thy	Thu Nov 12 13:56:07 2009 +0100
@@ -305,6 +305,9 @@
 
 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
 
+thm m2
+
+thm append_assoc
 (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *)
 ML {* lift_thm_fset @{context} @{thm m1} *}
 ML {* lift_thm_fset @{context} @{thm m2} *}

--- a/QuotMain.thy	Thu Nov 12 12:07:33 2009 +0100
+++ b/QuotMain.thy	Thu Nov 12 13:56:07 2009 +0100
@@ -1030,10 +1030,8 @@
 ML {*
 fun lookup_quot_data lthy qty =
   let
-    fun matches (ty1, ty2) =
-      Type.raw_instance (ty1, Logic.varifyT ty2);
     val qty_name = fst (dest_Type qty)
-    val SOME quotdata = quotdata_lookup lthy qty_name 
+    val SOME quotdata = quotdata_lookup lthy qty_name
                   (* cu: Changed the lookup\<dots>not sure whether this works *)
     (* TODO: Should no longer be needed *)
     val rty = Logic.unvarifyT (#rtyp quotdata)

--- a/quotient.ML	Thu Nov 12 12:07:33 2009 +0100
+++ b/quotient.ML	Thu Nov 12 13:56:07 2009 +0100
@@ -238,4 +238,4 @@
 
 end; (* structure *)
 
-open Quotient
\ No newline at end of file
+open Quotient

--- a/quotient_info.ML	Thu Nov 12 12:07:33 2009 +0100
+++ b/quotient_info.ML	Thu Nov 12 13:56:07 2009 +0100
@@ -81,7 +81,7 @@
 val quotdata_lookup_thy = Symtab.lookup o QuotData.get
 val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of
 
-fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) = 
+fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) =
       QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}))
 
 fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = 
@@ -164,4 +164,4 @@
 
 end; (* structure *)
 
-open Quotient_Info
\ No newline at end of file
+open Quotient_Info