decomp_simp': use lhs instead of elhs (preserves more bound variable names);
authorwenzelm
Thu Feb 28 19:22:56 2002 +0100 (2002-02-28)
changeset 129794c76bce4ce39
parent 12978 16cc829b9c65
child 12980 8f717cbd4e44
decomp_simp': use lhs instead of elhs (preserves more bound variable names);
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu Feb 28 18:16:23 2002 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu Feb 28 19:22:56 2002 +0100
     1.3 @@ -286,9 +286,9 @@
     1.4    in (sign, prems, term_of lhs, elhs, term_of rhs, perm) end;
     1.5  
     1.6  fun decomp_simp' thm =
     1.7 -  let val (_, _, _, elhs, rhs, _) = decomp_simp thm in
     1.8 +  let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
     1.9      if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
    1.10 -    else (term_of elhs, rhs)
    1.11 +    else (lhs, rhs)
    1.12    end;
    1.13  
    1.14  fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) thm =