--- a/Quot/quotient_typ.ML	Wed Dec 30 12:10:57 2009 +0000
+++ b/Quot/quotient_typ.ML	Thu Dec 31 23:53:10 2009 +0100
@@ -154,7 +154,7 @@
 
   (* storing the quot-info *)
   (* FIXME: VarifyT should not be used - at the moment it allows matching against the types. *)
-  fun qinfo phi = quotdata_transfer phi
+  fun qinfo phi = transform_quotdata phi
                     {qtyp = Logic.varifyT Abs_ty, rtyp = Logic.varifyT rty, 
                      equiv_rel = map_types Logic.varifyT rel, equiv_thm = equiv_thm}
   val lthy4 = Local_Theory.declaration true