diff -r bf6861ee3b90 -r d6407afb913c Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Wed Dec 23 23:53:03 2009 +0100
+++ b/Quot/quotient_typ.ML	Thu Dec 24 00:58:50 2009 +0100
@@ -155,11 +155,12 @@
   val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
 
   (* storing the quot-info *)
-  val lthy4 = quotdata_update qty_full_name 
-               (Logic.varifyT Abs_ty, Logic.varifyT rty, map_types Logic.varifyT rel, equiv_thm) lthy3  
   (* FIXME: VarifyT should not be used - at the moment it allows matching against the types. *)
-  (* FIXME: The relation can be any term, that later maybe needs to be given *)
-  (* FIXME: a different type (in regularize_trm); how should this be done?   *)
+  fun qinfo phi = quotdata_transfer 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
+                (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3  
 in
   lthy4
   |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])