--- 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
--- 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[" ^