--- a/Nominal/Nominal2_Eqvt.thy	Wed Mar 03 10:39:43 2010 +0100
+++ b/Nominal/Nominal2_Eqvt.thy	Wed Mar 03 11:42:15 2010 +0100
@@ -239,7 +239,8 @@
   imp_eqvt [folded induct_implies_def]
 
   (* nominal *)
-  permute_eqvt supp_eqvt fresh_eqvt
+  (*permute_eqvt commented out since it loops *)
+  supp_eqvt fresh_eqvt
   permute_pure
 
   (* datatypes *)

--- a/Nominal/Parser.thy	Wed Mar 03 10:39:43 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 03 11:42:15 2010 +0100
@@ -231,7 +231,7 @@
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
   val raw_binds_flat = map (map flat) raw_binds;
   val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat lthy3;
-(*  val alpha_ts_loc = #preds alpha
+  val alpha_ts_loc = #preds alpha
   val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
   val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc;
   val alpha_induct_loc = #induct alpha
@@ -245,7 +245,7 @@
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms
     ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5;
-  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms 
+(*  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms 
     (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6;
   val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
   val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
@@ -256,7 +256,7 @@
     (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_names ~~ all_typs) ~~ alpha_ts))
     (ALLGOALS (resolve_tac alpha_equivp)) lthy6;*)
 in
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy6)
 end
 *}
 

--- a/Nominal/Test.thy	Wed Mar 03 10:39:43 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 03 11:42:15 2010 +0100
@@ -17,6 +17,41 @@
 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)
+defer
+apply (simp add: alpha_weird_raw.intros)
+apply (simp add: alpha_weird_raw.intros)
+apply (simp only: permute_weird_raw.simps)
+apply (rule alpha_weird_raw.intros)
+apply (erule exi[of _ _ "p"])
+apply (erule exi[of _ _ "p"])
+apply (erule exi[of _ _ "p"])
+apply (erule exi[of _ _ "p"])
+apply (erule conjE)+
+apply (rule conjI)
+apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"])
+apply (simp add: eqvts)
+apply (simp add: eqvts)
+apply (rule conjI)
+defer
+apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"])
+apply (simp add: eqvts)
+apply (simp add: eqvts)
+apply (rule conjI)
+defer
+apply (simp add: supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt)
+apply(simp add: alpha_gen.simps)
+apply(erule conjE)+
+  apply(rule conjI)
+  apply(rule_tac ?p1="- p" in permute_eq_iff[THEN iffD1])
+apply (simp add: eqvts)
+  apply(rule conjI)
+  apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1])
+apply (simp add: eqvts add_perm_eqvt)
+apply (simp add: permute_eqvt[symmetric])
+done
+
 primrec 
   fv_weird
 where
@@ -209,14 +244,15 @@
 
 (* example 4 from Terms.thy *)
 
-(* fv_eqvt does not work, we need to repaire defined permute functions...
-nominal_datatype trm4 =
+(* fv_eqvt does not work, we need to repaire defined permute functions
+   defined fv and defined alpha... *)
+(*nominal_datatype trm4 =
   Vr4 "name"
 | Ap4 "trm4" "trm4 list"
 | Lm4 x::"name" t::"trm4"  bind x in t
 
 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
-thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
+thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]*)
 
 (* example 5 from Terms.thy *)