decomp_simp': use lhs instead of elhs (preserves more bound variable names);

--- a/src/Pure/meta_simplifier.ML	Thu Feb 28 18:16:23 2002 +0100
+++ b/src/Pure/meta_simplifier.ML	Thu Feb 28 19:22:56 2002 +0100
@@ -286,9 +286,9 @@
   in (sign, prems, term_of lhs, elhs, term_of rhs, perm) end;
 
 fun decomp_simp' thm =
-  let val (_, _, _, elhs, rhs, _) = decomp_simp thm in
+  let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
     if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
-    else (term_of elhs, rhs)
+    else (lhs, rhs)
   end;
 
 fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) thm =