diff -r dca2c7c598f0 -r 2bdec7f430d3 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Jun 09 22:25:25 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Jun 09 23:12:02 2011 +0200
@@ -108,7 +108,7 @@
     | SOME thm' =>
         (case try (get_match_inst thy (get_lhs thm')) redex of
           NONE => NONE
-        | SOME inst2 => try (Drule.instantiate inst2) thm'))
+        | SOME inst2 => try (Drule.instantiate_normalize inst2) thm'))
   end
 
 fun ball_bex_range_simproc ss redex =
@@ -490,7 +490,7 @@
           if ty_c = ty_d
           then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
           else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm)
-        val thm4 = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
+        val thm4 = Drule.instantiate_normalize ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
       in
         Conv.rewr_conv thm4 ctrm
       end