# HG changeset patch
# User wenzelm
# Date 1150234909 -7200
# Node ID 1b0d48257caf1dd4cbf2f4d8817533958974392d
# Parent  6a346150611a1d07e51b61399e2fb6373e422047
added equiv;

diff -r 6a346150611a -r 1b0d48257caf src/Pure/pattern.ML
--- 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) =