# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263168214 -3600
# Node ID fb7fe6aca6f0dc404e1f3bdcc6c50c6f893f14d6
# Parent  129caba33c034c9474a88aad68e4a453e105afc3
tuned previous commit further

diff -r 129caba33c03 -r fb7fe6aca6f0 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Mon Jan 11 00:31:29 2010 +0100
+++ b/Quot/QuotMain.thy	Mon Jan 11 01:03:34 2010 +0100
@@ -107,7 +107,6 @@
 lemmas [id_simps] =
   fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
-  (*id_def[THEN eq_reflection, symmetric]*)
   id_o[THEN eq_reflection]
   o_id[THEN eq_reflection]
   eq_comp_r
diff -r 129caba33c03 -r fb7fe6aca6f0 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Mon Jan 11 00:31:29 2010 +0100
+++ b/Quot/quotient_term.ML	Mon Jan 11 01:03:34 2010 +0100
@@ -199,9 +199,7 @@
              val map_fun = mk_mapfun ctxt vs rty_pat       
              val result = list_comb (map_fun, args) 
            in
-             (*if tys' = [] orelse tys' = tys 
-             then absrep_const flag ctxt s'
-             else*) mk_fun_compose flag (absrep_const flag ctxt s', result)
+             mk_fun_compose flag (absrep_const flag ctxt s', result)
            end
     | (TFree x, TFree x') =>
         if x = x'
@@ -300,9 +298,7 @@
            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 
-           then eqv_rel'
-           else*) mk_rel_compose (result, eqv_rel')
+           mk_rel_compose (result, eqv_rel')
          end
       | _ => HOLogic.eq_const rty
 
@@ -402,6 +398,7 @@
   | (* in this case we just check whether the given equivalence relation is correct *) 
     (rel, Const (@{const_name "op ="}, ty')) =>
        let 
+         (* FIXME: better exception handling *)  
          fun exc rel rel' = LIFT_MATCH ("regularise (relation mismatch)\n[" ^
            Syntax.string_of_term ctxt rel ^ " :: " ^
            Syntax.string_of_typ ctxt (fastype_of rel) ^ "]\n[" ^