--- a/Quot/quotient_term.ML	Sat Jan 09 09:38:34 2010 +0100
+++ b/Quot/quotient_term.ML	Mon Jan 11 00:31:29 2010 +0100
@@ -24,6 +24,15 @@
 
 exception LIFT_MATCH of string
 
+(* simplifies a term according to the id_rules *)
+fun id_simplify ctxt trm =
+let
+  val thy = ProofContext.theory_of ctxt 
+  val id_thms = id_simps_get ctxt
+in
+  MetaSimplifier.rewrite_term thy id_thms [] trm
+end		
+ 
 (******************************)
 (* Aggregate Rep/Abs Function *)
 (******************************)
@@ -190,9 +199,9 @@
              val map_fun = mk_mapfun ctxt vs rty_pat       
              val result = list_comb (map_fun, args) 
            in
-             if tys' = [] orelse tys' = tys 
+             (*if tys' = [] orelse tys' = tys 
              then absrep_const flag ctxt s'
-             else mk_fun_compose flag (absrep_const flag ctxt s', result)
+             else*) mk_fun_compose flag (absrep_const flag ctxt s', result)
            end
     | (TFree x, TFree x') =>
         if x = x'
@@ -204,7 +213,7 @@
 fun absrep_fun_chk flag ctxt (rty, qty) =
   absrep_fun flag ctxt (rty, qty)
   |> Syntax.check_term ctxt
-
+  |> id_simplify ctxt
 
 (**********************************)
 (* Aggregate Equivalence Relation *)
@@ -291,15 +300,16 @@
            val eqv_rel = get_equiv_rel ctxt s'
            val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
          in
-           if tys' = [] orelse tys' = tys 
+           (*if tys' = [] orelse tys' = tys 
            then eqv_rel'
-           else mk_rel_compose (result, eqv_rel')
+           else*) mk_rel_compose (result, eqv_rel')
          end
       | _ => HOLogic.eq_const rty
 
 fun equiv_relation_chk ctxt (rty, qty) =
   equiv_relation ctxt (rty, qty)
   |> Syntax.check_term ctxt
+  |> id_simplify ctxt
 
 
 (******************)
@@ -452,6 +462,7 @@
 fun regularize_trm_chk ctxt (rtrm, qtrm) =
   regularize_trm ctxt (rtrm, qtrm) 
   |> Syntax.check_term ctxt
+  |> id_simplify ctxt
 
 
 (*********************)
@@ -490,6 +501,14 @@
 fun mk_repabs ctxt (T, T') trm = 
   absrep_fun repF ctxt (T, T') $ (absrep_fun absF ctxt (T, T') $ trm)
 
+fun inj_repabs_err ctxt msg rtrm qtrm =
+let
+  val rtrm_str = Syntax.string_of_term ctxt rtrm
+  val qtrm_str = Syntax.string_of_term ctxt qtrm 
+in
+  raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
+end
+
 
 (* bound variables need to be treated properly,     *)
 (* as the type of subterms needs to be calculated   *)
@@ -540,11 +559,12 @@
         else mk_repabs ctxt (rty, T') rtrm
       end   
   
-  | _ => raise (LIFT_MATCH "injection (default)")
+  | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
 
 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
   inj_repabs_trm ctxt (rtrm, qtrm) 
   |> Syntax.check_term ctxt
+  |> id_simplify ctxt
 
 end; (* structure *)