equal
deleted
inserted
replaced
920 and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)" |
920 and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)" |
921 using assms by (auto simp add: Abs1_eq_iff fresh_permute_left) |
921 using assms by (auto simp add: Abs1_eq_iff fresh_permute_left) |
922 |
922 |
923 |
923 |
924 ML {* |
924 ML {* |
925 fun alpha_single_simproc thm _ ss ctrm = |
925 fun alpha_single_simproc thm _ ctxt ctrm = |
926 let |
926 let |
927 val ctxt = Simplifier.the_context ss |
|
928 val thy = Proof_Context.theory_of ctxt |
927 val thy = Proof_Context.theory_of ctxt |
929 val _ $ (_ $ x) $ (_ $ y) = term_of ctrm |
928 val _ $ (_ $ x) $ (_ $ y) = term_of ctrm |
930 val cvrs = union (op =) (Term.add_frees x []) (Term.add_frees y []) |
929 val cvrs = union (op =) (Term.add_frees x []) (Term.add_frees y []) |
931 |> filter (fn (_, ty) => Sign.of_sort thy (ty, @{sort fs})) |
930 |> filter (fn (_, ty) => Sign.of_sort thy (ty, @{sort fs})) |
932 |> map Free |
931 |> map Free |