# HG changeset patch
# User wenzelm
# Date 1014920576 -3600
# Node ID 4c76bce4ce391d6e2b8e938ccf65925279426aaf
# Parent  16cc829b9c6520b84ab0a1d50a6c16340a827953
decomp_simp': use lhs instead of elhs (preserves more bound variable names);

diff -r 16cc829b9c65 -r 4c76bce4ce39 src/Pure/meta_simplifier.ML
--- 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 =