--- a/Quot/quotient_term.ML	Wed Dec 23 13:45:42 2009 +0100
+++ b/Quot/quotient_term.ML	Wed Dec 23 21:30:23 2009 +0100
@@ -287,8 +287,9 @@
   
   * If the application involves a bounded quantifier, we recurse on 
     the second argument. If the application is a bounded abstraction,
-    we always put an Re/Abs around it (since bounded abstractions
-    always need lifting). Otherwise we recurse on both arguments.
+    we always put an Rep/Abs around it (since bounded abstractions
+    are assumed to always need lifting). Otherwise we recurse on both 
+    arguments.
 
   For constants:
 

--- a/Quot/quotient_typ.ML	Wed Dec 23 13:45:42 2009 +0100
+++ b/Quot/quotient_typ.ML	Wed Dec 23 21:30:23 2009 +0100
@@ -123,46 +123,47 @@
 fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy =
 let
   (* generates the typedef *)
-  val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy
+  val ((qty_full_name, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy
 
   (* 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
-  val rep_name = #Rep_name typedef_info
-  val abs = Const (abs_name, rep_ty --> abs_ty)
-  val rep = Const (rep_name, abs_ty --> rep_ty)
+  val Abs_ty = #abs_type typedef_info
+  val Rep_ty = #rep_type typedef_info
+  val Abs_name = #Abs_name typedef_info
+  val Rep_name = #Rep_name typedef_info
+  val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
+  val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
 
-  (* 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)
-  val REP_trm = Syntax.check_term lthy1 (REP_const $ rep)
-  val ABS_name = Binding.prefix_name "abs_" qty_name
-  val REP_name = Binding.prefix_name "rep_" qty_name
+  (* 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_const)
+  val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const)
+  val abs_name = Binding.prefix_name "abs_" qty_name
+  val rep_name = Binding.prefix_name "rep_" qty_name
 
-  val ((ABS, ABS_def), lthy2) = define (ABS_name, NoSyn, ABS_trm) lthy1
-  val ((REP, REP_def), lthy3) = define (REP_name, NoSyn, REP_trm) lthy2
+  val ((abs, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1
+  val ((rep, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2
 
   (* quot_type theorem - needed below *)
-  val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy3
+  val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3
 
   (* quotient theorem *)  
-  val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy3
+  val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3
   val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
 
+  (* name equivalence theorem *)
+  val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
+
   (* storing the quot-info *)
-  val qty_str = fst (Term.dest_Type abs_ty)
-  val lthy4 = quotdata_update qty_str 
-               (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy3  
+  val lthy4 = quotdata_update qty_full_name 
+               (Logic.varifyT Abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy3  
   (* FIXME: varifyT should not be used *)
   (* 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?    *)
-
+  (* FIXME: a different type (in regularize_trm); how should this be done?   *)
 in
   lthy4
   |> 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])
+  ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add])
 end