--- 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 =