--- a/Quot/quotient_def.ML	Wed Jan 13 13:12:04 2010 +0100
+++ b/Quot/quotient_def.ML	Wed Jan 13 15:17:36 2010 +0100
@@ -50,7 +50,7 @@
   (* data storage *)
   fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
   val lthy'' = Local_Theory.declaration true
-                 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'
+                 (fn phi => qconsts_update_gen trm (qcinfo phi)) lthy'
 in
   ((trm, thm), lthy'')
 end