--- a/src/Pure/pattern.ML Tue Jun 13 23:41:47 2006 +0200
+++ b/src/Pure/pattern.ML Tue Jun 13 23:41:49 2006 +0200
@@ -23,6 +23,7 @@
val first_order_match: theory -> term * term
-> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
val matches: theory -> term * term -> bool
+ val equiv: theory -> term * term -> bool
val matches_subterm: theory -> term * term -> bool
val unify: theory -> term * term -> Envir.env -> Envir.env
val first_order: term -> bool
@@ -405,6 +406,8 @@
fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
+fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);
+
(* Does pat match a subterm of obj? *)
fun matches_subterm thy (pat,obj) =