--- a/quotient_def.ML	Sat Nov 21 14:45:25 2009 +0100
+++ b/quotient_def.ML	Sat Nov 21 23:23:01 2009 +0100
@@ -24,11 +24,6 @@
   ((rhs, thm), lthy')
 end
 
-(* calculates the aggregate abs and rep functions for a given type; 
-   repF is for constants' arguments; absF is for constants;
-   function types need to be treated specially, since repF and absF
-   change *)
-
 datatype flag = absF | repF
 
 fun negF absF = repF
@@ -72,6 +67,12 @@
   | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
 end
 
+
+(* calculates the aggregate abs and rep functions for a given type; 
+   repF is for constants' arguments; absF is for constants;
+   function types need to be treated specially, since repF and absF
+   change *)
+
 fun get_fun flag lthy (rty, qty) =
   case (rty, qty) of 
     (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
@@ -96,7 +97,7 @@
   | (TVar _, TVar _) => ty_lift_error2 lthy rty qty
   | _ => ty_lift_error1 lthy rty qty
 
-fun make_def nconst_bname qty mx attr rhs lthy =
+fun make_def qconst_bname qty mx attr rhs lthy =
 let
   val rty = fastype_of rhs
   val (arg_rtys, res_rty) = strip_type rty
@@ -111,12 +112,12 @@
   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 ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy
 
-  val nconst_str = Binding.name_of nconst_bname
+  val qconst_str = Binding.name_of qconst_bname
   fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs}
   val lthy'' = Local_Theory.declaration true
-                 (fn phi => qconsts_update_gen nconst_str (qcinfo phi)) lthy'
+                 (fn phi => qconsts_update_gen qconst_str (qcinfo phi)) lthy'
 in
   ((trm, thm), lthy'')
 end