--- a/Nominal/Perm.thy	Tue May 25 00:24:41 2010 +0100
+++ b/Nominal/Perm.thy	Wed May 26 15:34:54 2010 +0200
@@ -48,33 +48,5 @@
 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
-*}
 
 end