--- a/QuotMain.thy	Thu Nov 05 13:47:41 2009 +0100
+++ b/QuotMain.thy	Thu Nov 05 16:43:57 2009 +0100
@@ -669,14 +669,13 @@
 )
 *}
 
-
-
 ML {*
 fun quotient_tac quot_thm =
   REPEAT_ALL_NEW (FIRST' [
     rtac @{thm FUN_QUOTIENT},
     rtac quot_thm,
-    rtac @{thm IDENTITY_QUOTIENT}
+    rtac @{thm IDENTITY_QUOTIENT},
+    (fn i => CHANGED (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I}) i) THEN rtac @{thm IDENTITY_QUOTIENT} i)
   ])
 *}
 
@@ -766,7 +765,8 @@
      (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
      THEN_ALL_NEW (fn _ => no_tac)
     ),
-    WEAK_LAMBDA_RES_TAC ctxt
+    WEAK_LAMBDA_RES_TAC ctxt,
+    (fn i => CHANGED (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}) i))
     ])
 *}
 
@@ -793,26 +793,32 @@
   apply (simp_all add: map.simps)
 done
 
+ML {*
+fun simp_ids lthy thm =
+  thm
+  |> MetaSimplifier.rewrite_rule @{thms id_def_sym}
+  |> repeat_eqsubst_thm lthy @{thms FUN_MAP_I id_apply prod_fun_id map_id}
+*}
+
 text {* expects atomized definition *}
 ML {*
-  fun add_lower_defs_aux ctxt thm =
+  fun add_lower_defs_aux lthy thm =
     let
       val e1 = @{thm fun_cong} OF [thm];
-      val f = eqsubst_thm ctxt @{thms fun_map.simps} e1;
-      val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f;
-      val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I id_apply prod_fun_id map_id} g
+      val f = eqsubst_thm lthy @{thms fun_map.simps} e1;
+      val g = simp_ids lthy f
     in
-      thm :: (add_lower_defs_aux ctxt h)
+      (simp_ids lthy thm) :: (add_lower_defs_aux lthy g)
     end
-    handle _ => [thm]
+    handle _ => [simp_ids lthy thm]
 *}
 
 ML {*
-fun add_lower_defs ctxt defs =
+fun add_lower_defs lthy def =
   let
-    val defs_pre_sym = map symmetric defs
-    val defs_atom = map atomize_thm defs_pre_sym
-    val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)
+    val def_pre_sym = symmetric def
+    val def_atom = atomize_thm def_pre_sym
+    val defs_all = add_lower_defs_aux lthy def_atom
   in
     map Thm.varifyT defs_all
   end
@@ -1012,9 +1018,10 @@
   val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
   val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
   val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
-  val defs_sym = add_lower_defs lthy defs;
+  val defs_sym = flat (map (add_lower_defs lthy) defs);
   val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
-  val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l;
+  val t_id = simp_ids lthy t_l;
+  val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;
   val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
   val t_rv = ObjectLogic.rulify t_r