diff -r 017cb46b27bb -r 433f7c17255f Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Jan 13 00:46:31 2010 +0100
+++ b/Quot/quotient_term.ML	Wed Jan 13 09:19:20 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 =
@@ -52,7 +52,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)
@@ -89,7 +89,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)
@@ -351,14 +351,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)
@@ -375,9 +375,9 @@
   | _ => 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      
+(* produces a regularized version of rtrm
 
    - the result might contain dummyTs           
 
@@ -487,15 +487,14 @@
   |> Syntax.check_term ctxt
 
 
-(*********************)
-(* Rep/Abs Injection *)
-(*********************)
+
+(*** Rep/Abs Injection ***)
 
 (*
 Injection of Rep/Abs means:
 
-  For abstractions
-:
+  For abstractions:
+
   * If the type of the abstraction needs lifting, then we add Rep/Abs 
     around the abstraction; otherwise we leave it unchanged.
  
@@ -532,9 +531,8 @@
 end
 
 
-(* bound variables need to be treated properly,     *)
-(* as the type of subterms needs to be calculated   *)
-
+(* bound variables need to be treated properly,
+   as the type of subterms needs to be calculated   *)
 fun inj_repabs_trm ctxt (rtrm, qtrm) =
  case (rtrm, qtrm) of
     (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>