diff -r 2050b5723c04 -r 9909cc3566c5 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Wed Apr 14 14:41:54 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Wed Apr 14 15:02:07 2010 +0200
@@ -8,6 +8,10 @@
 sig
   val mk_minus: term -> term
   val mk_perm: term -> term -> term
+  val dest_perm: term -> term * term
+
+  val mk_equiv: thm -> thm
+  val safe_mk_equiv: thm -> thm
 end
 
 
@@ -24,7 +28,11 @@
   Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm
 end
 
+fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
+  | dest_perm t = raise TERM ("dest_perm", [t])
 
+fun mk_equiv r = r RS @{thm eq_reflection};
+fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
 
 end (* structure *)