--- a/src/Pure/meta_simplifier.ML Tue Mar 21 12:18:10 2006 +0100
+++ b/src/Pure/meta_simplifier.ML Tue Mar 21 12:18:11 2006 +0100
@@ -389,7 +389,7 @@
| vperm (t, u) = (t = u);
fun var_perm (t, u) =
- vperm (t, u) andalso eq_set (term_varnames t, term_varnames u);
+ vperm (t, u) andalso gen_eq_set (op =) (term_varnames t, term_varnames u);
(* FIXME: it seems that the conditions on extra variables are too liberal if
prems are nonempty: does solving the prems really guarantee instantiation of
@@ -532,7 +532,7 @@
is_Var x andalso forall is_Bound xs andalso
null (findrep xs) andalso xs = ys andalso
(x, y) mem varpairs andalso
- is_full_cong_prems prems (varpairs \ (x, y))
+ is_full_cong_prems prems (remove (op =) (x, y) varpairs)
end
| _ => false);