diff -r 9e247b9505f0 -r 09d5b7f0e55d Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Wed Jan 13 16:46:25 2010 +0100
+++ b/Quot/quotient_def.ML	Thu Jan 14 08:02:20 2010 +0100
@@ -52,7 +52,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 trm (qcinfo phi)) lthy'
+                 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'
 in
   ((trm, thm), lthy'')
 end