src/Pure/conv.ML

--- a/src/Pure/conv.ML	Thu Jun 09 22:25:25 2011 +0200
+++ b/src/Pure/conv.ML	Thu Jun 09 23:12:02 2011 +0200
@@ -162,7 +162,7 @@
     val lhs = Thm.lhs_of rule1;
     val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
   in
-    Drule.instantiate (Thm.match (lhs, ct)) rule2
+    Drule.instantiate_normalize (Thm.match (lhs, ct)) rule2
       handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
   end;