diff -r 20fa8dd8fb93 -r fec6301a1989 quotient_def.ML
--- a/quotient_def.ML	Wed Nov 11 22:30:43 2009 +0100
+++ b/quotient_def.ML	Thu Nov 12 02:18:36 2009 +0100
@@ -135,8 +135,14 @@
 
   val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs)
                    |> Syntax.check_term lthy 
+
+  val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy
+
+  val nconst_str = Binding.str_of nconst_bname
+  val qc_info = {qconst = trm, rconst = rhs}
+  val lthy'' = qconsts_update nconst_str qc_info lthy'
 in
-  define nconst_bname mx attr absrep_trm lthy
+  ((trm, thm), lthy'')
 end
 
 (* interface and syntax setup *)