# HG changeset patch
# User wenzelm
# Date 1356883151 -3600
# Node ID f1c2f911ae33b3ee7d8b12063c434ca5ff20a1a4
# Parent  eedc01eca7364b8eee8b2e66b1fb9a40a9af93b5
tuned -- recovered comments from 791157a4179a;

diff -r eedc01eca736 -r f1c2f911ae33 src/Pure/conv.ML
--- a/src/Pure/conv.ML	Sun Dec 30 16:40:28 2012 +0100
+++ b/src/Pure/conv.ML	Sun Dec 30 16:59:11 2012 +0100
@@ -154,8 +154,8 @@
   | _ => raise CTERM ("implies_concl_conv", [ct]));
 
 
-(* single rewrite step
-   beta-normalizes the rhs and takes care that lhs aconv ct *)
+(* single rewrite step, cf. REWR_CONV in HOL *)
+
 fun rewr_conv rule ct =
   let
     val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
@@ -163,13 +163,13 @@
     val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
     val rule3 =
       Thm.instantiate (Thm.match (lhs, ct)) rule2
-      handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
+        handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct]);
     val rule4 =
-      if term_of(Thm.lhs_of rule3) aconv term_of ct then rule3
+      if Thm.lhs_of rule3 aconvc 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
+        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);