diff -r d89851ebac9b -r 2d21fd8114af Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Mon Dec 21 23:01:58 2009 +0100
+++ b/Quot/quotient_tacs.ML	Mon Dec 21 23:13:40 2009 +0100
@@ -80,7 +80,7 @@
   val eqv_goal = HOLogic.mk_Trueprop 
                      (Const (@{const_name "equivp"}, eqv_ty) $ R2)  
   val eqv_prem = Goal.prove ctxt [] [] eqv_goal (fn _ => equiv_tac ctxt 1)
-  val thm = (@{thm eq_reflection} OF [ball_bex_thm OF [eqv_prem]])
+  val thm = ball_bex_thm OF [eqv_prem]
   val thmi = Drule.instantiate' [] [SOME (cterm_of thy R1)] thm
   val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex
   val thm2 = Drule.instantiate inst thmi
@@ -98,11 +98,11 @@
  case redex of
     (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ 
       (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
-        calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2
+        calculate_instance ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
 
   | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ 
       (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>  
-        calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2
+        calculate_instance ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
   | _ => NONE
 end
 
@@ -456,8 +456,8 @@
        val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
        val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
        val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
-       val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}
-       val te = @{thm eq_reflection} OF [solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)]
+       val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
+       val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)
        val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
        val make_inst = if ty_c = ty_d then make_inst_id else make_inst
        val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)