diff -r 67e5da3a356a -r 3fd1365f5729 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Tue Jan 12 16:44:33 2010 +0100
+++ b/Quot/quotient_term.ML	Tue Jan 12 17:46:35 2010 +0100
@@ -1,20 +1,20 @@
 signature QUOTIENT_TERM =
 sig
-   exception LIFT_MATCH of string
- 
-   datatype flag = absF | repF
-   
-   val absrep_fun: flag -> Proof.context -> (typ * typ) -> term
-   val absrep_fun_chk: flag -> Proof.context -> (typ * typ) -> term
+  exception LIFT_MATCH of string
+
+  datatype flag = absF | repF
+
+  val absrep_fun: flag -> Proof.context -> typ * typ -> term
+  val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
 
-   val equiv_relation: Proof.context -> (typ * typ) -> term
-   val equiv_relation_chk: Proof.context -> (typ * typ) -> term
+  val equiv_relation: Proof.context -> typ * typ -> term
+  val equiv_relation_chk: Proof.context -> typ * typ -> term
 
-   val regularize_trm: Proof.context -> (term * term) -> term
-   val regularize_trm_chk: Proof.context -> (term * term) -> term
-   
-   val inj_repabs_trm: Proof.context -> (term * term) -> term
-   val inj_repabs_trm_chk: Proof.context -> (term * term) -> term
+  val regularize_trm: Proof.context -> term * term -> term
+  val regularize_trm_chk: Proof.context -> term * term -> term
+
+  val inj_repabs_trm: Proof.context -> term * term -> term
+  val inj_repabs_trm_chk: Proof.context -> term * term -> term
 end;
 
 structure Quotient_Term: QUOTIENT_TERM =
@@ -55,7 +55,7 @@
 fun get_mapfun ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
-  val exc = LIFT_MATCH ("No map function for type " ^ (quote s) ^ " found.")
+  val exc = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
   val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc
 in
   Const (mapfun, dummyT)
@@ -88,7 +88,7 @@
 fun get_rty_qty ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
-  val exc = LIFT_MATCH ("No quotient type " ^ (quote s) ^ " found.")
+  val exc = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
   val qdata = (quotdata_lookup thy s) handle NotFound => raise exc
 in
   (#rtyp qdata, #qtyp qdata)
@@ -163,7 +163,7 @@
 
   The matching is necessary for types like
 
-      ('a * 'a) list / 'a bar                                    *)
+      ('a * 'a) list / 'a bar *)
 fun absrep_fun flag ctxt (rty, qty) =
   if rty = qty  
   then mk_identity rty
@@ -267,7 +267,7 @@
 end
 
 (* builds the aggregate equivalence relation
-   that will be the argument of Respects     *)
+   that will be the argument of Respects *)
 fun equiv_relation ctxt (rty, qty) =
   if rty = qty
   then HOLogic.eq_const rty
@@ -307,17 +307,17 @@
 (*** Regularization ***)
 
 (* Regularizing an rtrm means:
- 
- - Quantifiers over types that need lifting are replaced 
+
+ - Quantifiers over types that need lifting are replaced
    by bounded quantifiers, for example:
 
       All P  ----> All (Respects R) P
 
    where the aggregate relation R is given by the rty and qty;
- 
+
  - Abstractions over types that need lifting are replaced
    by bounded abstractions, for example:
-      
+
       %x. P  ----> Ball (Respects R) %x. P
 
  - Equalities over types that need lifting are replaced by
@@ -325,14 +325,14 @@
 
       A = B  ----> R A B
 
-   or 
+   or
 
       A = B  ----> (R ===> R) A B
- 
+
    for more complicated types of A and B
 *)
 
-            
+
 val mk_babs = Const (@{const_name Babs}, dummyT)
 val mk_ball = Const (@{const_name Ball}, dummyT)
 val mk_bex  = Const (@{const_name Bex}, dummyT)
@@ -348,16 +348,12 @@
   | _ => f (trm1, trm2)
 
 (* the major type of All and Ex quantifiers *)
-fun qnt_typ ty = domain_type (domain_type ty)  
+fun qnt_typ ty = domain_type (domain_type ty)
 
 
-(* produces a regularized version of rtrm       *)
-(*                                              *)
-(* - the result might contain dummyTs           *)
-(*                                              *)
-(* - for regularisation we do not need any      *)
-(*   special treatment of bound variables       *)
-
+(* produces a regularized version of rtrm
+   - the result might contain dummyTs
+   - for regularisation we do not need to treat bound variables specially *)
 fun regularize_trm ctxt (rtrm, qtrm) =
   case (rtrm, qtrm) of
     (Abs (x, ty, t), Abs (_, ty', t')) =>