src/Pure/meta_simplifier.ML

       val perm = var_perm (term_of elhs, erhs) andalso not (term_of elhs aconv erhs)
                  andalso not (is_Var (term_of elhs))
   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 =
   case mk_eq_True thm of
     None => []