diff -r 119f7d6a3556 -r c1989de100b4 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Thu Dec 17 17:59:12 2009 +0100
+++ b/Quot/quotient_typ.ML	Sat Dec 19 22:04:34 2009 +0100
@@ -12,7 +12,7 @@
 
 exception LIFT_MATCH of string
 
-(* wrappers for define, note and theorem_i *)
+(* wrappers for define, note, Attrib.internal and theorem_i *)
 fun define (name, mx, rhs) lthy =
 let
   val ((rhs, (_ , thm)), lthy') =
@@ -28,7 +28,7 @@
   (thm', lthy')
 end
 
-fun internal_attr at = Attrib.internal (K at)
+fun intern_attr at = Attrib.internal (K at)
 
 fun theorem after_qed goals ctxt =
 let
@@ -117,13 +117,13 @@
     (K typedef_quotient_thm_tac)
 end
 
-(* main function for constructing the quotient type *)
+(* main function for constructing a quotient type *)
 fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy =
 let
-  (* generates typedef *)
+  (* generates the typedef *)
   val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy
 
-  (* abs and rep functions *)
+  (* abs and rep functions from the typedef *)
   val abs_ty = #abs_type typedef_info
   val rep_ty = #rep_type typedef_info
   val abs_name = #Abs_name typedef_info
@@ -131,7 +131,7 @@
   val abs = Const (abs_name, rep_ty --> abs_ty)
   val rep = Const (rep_name, abs_ty --> rep_ty)
 
-  (* ABS and REP definitions *)
+  (* more abstract ABS and REP definitions *)
   val ABS_const = Const (@{const_name "QUOT_TYPE.abs"}, dummyT )
   val REP_const = Const (@{const_name "QUOT_TYPE.rep"}, dummyT )
   val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs)
@@ -155,14 +155,14 @@
   val lthy3 = quotdata_update qty_str 
                (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2  
   (* FIXME: varifyT should not be used *)
-  (* FIXME: the relation needs to be a string, since its type needs *)
-  (* FIXME: to recalculated in for example REGULARIZE *)
+  (* FIXME: the relation can be any term, that later maybe needs to be given *)
+  (* FIXME: a different type (in regularize_trm); how should tis be done?    *)
 
 in
   lthy3
   |> note (quot_thm_name, quot_thm, [])
-  ||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add])
-  ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [internal_attr equiv_rules_add])
+  ||>> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
+  ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [intern_attr equiv_rules_add])
 end