--- a/Nominal/Perm.thy	Sun Mar 07 21:30:12 2010 +0100
+++ b/Nominal/Perm.thy	Sun Mar 07 21:30:57 2010 +0100
@@ -134,6 +134,37 @@
 end
 *}
 
+ML {*
+fun neq_to_rel r neq =
+let
+  val neq = HOLogic.dest_Trueprop (prop_of neq)
+  val eq = HOLogic.dest_not neq
+  val (lhs, rhs) = HOLogic.dest_eq eq
+  val rel = r $ lhs $ rhs
+  val nrel = HOLogic.mk_not rel
+in
+  HOLogic.mk_Trueprop nrel
+end
+*}
+
+ML {*
+fun neq_to_rel_tac cases distinct =
+  rtac notI THEN' eresolve_tac cases THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct)
+*}
+
+ML {*
+fun distinct_rel ctxt cases (dists, rel) =
+let
+  val ((_, thms), ctxt') = Variable.import false dists ctxt
+  val terms = map (neq_to_rel rel) thms
+  val nrels = map (fn t => Goal.prove ctxt' [] [] t (fn _ => neq_to_rel_tac cases dists 1)) terms
+in
+  Variable.export ctxt' ctxt nrels
+end
+*}
+
+
+
 (* Test
 atom_decl name