--- a/Quot/quotient_typ.ML	Wed Dec 23 13:23:33 2009 +0100
+++ b/Quot/quotient_typ.ML	Wed Dec 23 13:45:42 2009 +0100
@@ -76,7 +76,7 @@
            NONE typedef_tac) lthy
 end
 
-(* tactic to prove the QUOT_TYPE theorem for the new type *)
+(* tactic to prove the Quot_Type theorem for the new type *)
 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
 let
   val rep_thm = (#Rep typedef_info) RS mem_def1
@@ -84,7 +84,7 @@
   val abs_inv = mem_def2 RS (#Abs_inverse typedef_info)
   val rep_inj = #Rep_inject typedef_info
 in
-  (rtac @{thm QUOT_TYPE.intro} THEN' 
+  (rtac @{thm Quot_Type.intro} THEN' 
    RANGE [rtac equiv_thm,
           rtac rep_thm,
           rtac rep_inv,
@@ -92,10 +92,10 @@
           rtac rep_inj]) 1
 end
 
-(* proves the QUOT_TYPE theorem *)
+(* proves the Quot_Type theorem *)
 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
 let
-  val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT)
+  val quot_type_const = Const (@{const_name "Quot_Type"}, dummyT)
   val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
              |> Syntax.check_term lthy
 in
@@ -112,7 +112,7 @@
 
   val typedef_quotient_thm_tac =
     EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]),
-            rtac @{thm QUOT_TYPE.Quotient},
+            rtac @{thm Quot_Type.Quotient},
             rtac quot_type_thm]
 in
   Goal.prove lthy [] [] goal
@@ -134,40 +134,38 @@
   val rep = 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_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
-  val (((ABS, ABS_def), (REP, REP_def)), lthy2) =
-         lthy1 |> define (ABS_name, NoSyn, ABS_trm)
-               ||>> define (REP_name, NoSyn, REP_trm)
+
+  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) lthy2
+  val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy3
 
   (* quotient theorem *)  
-  val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2
+  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
 
   (* storing the quot-info *)
   val qty_str = fst (Term.dest_Type abs_ty)
-  val lthy3 = quotdata_update qty_str 
-               (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2  
+  val lthy4 = quotdata_update qty_str 
+               (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?    *)
 
 in
-  lthy3
+  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])
 end
 
 
-
-
 (* interface and syntax setup *)
 
 (* the ML-interface takes a list of 4-tuples consisting of  *)