diff -r 0755f8fd56b3 -r 71225f4a4635 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Thu Dec 31 23:53:10 2009 +0100
+++ b/Quot/quotient_def.ML	Fri Jan 01 01:08:19 2010 +0100
@@ -26,16 +26,19 @@
 
 (* interface and syntax setup *)
 
-(* the ML-interface takes a 4-tuple consisting of *)
-(*                                                *)
-(* - the mixfix annotation                        *)
-(* - name and attributes of the meta eq           *)
-(* - the new constant including its type          *)
-(* - the rhs of the definition                    *)
+(* the ML-interface takes a 4-tuple consisting of  *)
+(*                                                 *)
+(* - the mixfix annotation                         *)
+(* - name and attributes                           *)
+(* - the new constant including its type           *)
+(* - the rhs of the definition                     *)
+(*                                                 *)
+(* returns the defined constant and its definition *)
+(* theorem; stores the data in the qconsts slot    *)
 
 fun quotient_def mx attr lhs rhs lthy =
 let
-  val Free (lhs_str, lhs_ty) = lhs;
+  val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.)
   val qconst_bname = Binding.name lhs_str;
   val absrep_trm = absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty) $ rhs
   val prop = Logic.mk_equals (lhs, absrep_trm)
@@ -44,6 +47,7 @@
 
   val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy
 
+  (* 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'
@@ -72,7 +76,3 @@
              OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
 
 end; (* structure *)
-
-
-
-