# HG changeset patch
# User nipkow
# Date 1351093256 -7200
# Node ID 791157a4179a3fbe2aea812c6645affe8414b799
# Parent  e84baadd4963aa97214a2aee8d563c4fe448509f
ensured that rewr_conv rule t = "t == u" literally not just modulo beta-eta

diff -r e84baadd4963 -r 791157a4179a src/Pure/conv.ML
--- a/src/Pure/conv.ML	Mon Oct 22 22:47:14 2012 +0200
+++ b/src/Pure/conv.ML	Wed Oct 24 17:40:56 2012 +0200
@@ -154,17 +154,22 @@
   | _ => raise CTERM ("implies_concl_conv", [ct]));
 
 
-(* single rewrite step, cf. REWR_CONV in HOL *)
-
+(* single rewrite step
+   beta-normalizes the rhs and takes care that lhs aconv ct *)
 fun rewr_conv rule ct =
   let
     val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
     val lhs = Thm.lhs_of rule1;
     val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
-  in
-    Drule.instantiate_normalize (Thm.match (lhs, ct)) rule2
+    val rule3 =
+      Thm.instantiate (Thm.match (lhs, ct)) rule2
       handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
-  end;
+    val rule4 =
+      if term_of(Thm.lhs_of rule3) aconv term_of ct then rule3
+      else
+        let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
+        in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (Thm.rhs_of rule3)) end
+  in Thm.transitive rule4 (Thm.beta_conversion true (Thm.rhs_of rule4)) end
 
 fun rewrs_conv rules = first_conv (map rewr_conv rules);