--- 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