diff -r 8502c2ff3be5 -r 88d2d4beb9e0 Nominal/Test.thy
--- a/Nominal/Test.thy	Wed Mar 03 12:47:06 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 03 12:48:05 2010 +0100
@@ -13,9 +13,6 @@
 thm permute_weird_raw.simps[no_vars]
 thm alpha_weird_raw.intros[no_vars]
 thm fv_weird_raw.simps[no_vars]
-(* Potential problem: Is it correct that in the fv-function 
-the first two terms are created? Should be ommitted. Also
-something wrong with the permutations. *)
 
 lemma "alpha_weird_raw a b \<Longrightarrow> alpha_weird_raw (p \<bullet> a) (p \<bullet> b)"
 apply (erule alpha_weird_raw.induct)
@@ -52,25 +49,6 @@
 apply (simp add: permute_eqvt[symmetric])
 done
 
-primrec 
-  fv_weird
-where
-  "fv_weird (WBind_raw x y p1 p2 p3) = 
-    (fv_weird p1 - {atom x}) \<union> (fv_weird p2 - ({atom x} \<union> {atom y})) \<union> (fv_weird p3 - {atom y})"
-| "fv_weird (WV_raw x) = {atom x}"
-| "fv_weird (WP_raw p1 p2) = (fv_weird p1 \<union> fv_weird p2)"
-
-inductive
-  alpha_weird
-where
-  "\<exists>p1 p2.  
-  ({atom y}, w3) \<approx>gen alpha_weird fv_weird p2 ({atom ya}, w3a) \<and>
-  ({atom x} \<union> {atom y}, w2) \<approx>gen alpha_weird fv_weird (p1 + p2) ({atom xa} \<union> {atom ya}, w2a) \<and>
-  ({atom x}, w1) \<approx>gen alpha_weird fv_weird p1 ({atom xa}, w1a) \<and>
-  supp p1 \<inter> supp p2 = {} \<Longrightarrow>
-  alpha_weird (WBind_raw x y w1 w2 w3) (WBind_raw xa ya w1a w2a w3a)"
-| "x = xa \<Longrightarrow> alpha_weird (WV_raw x) (WV_raw xa)"
-| "alpha_weird w2 w2a \<and> alpha_weird w1 w1a \<Longrightarrow> alpha_weird (WP_raw w1 w2) (WP_raw w1a w2a)"
 
 (*
 abbreviation "WBind \<equiv> WBind_raw"