diff -r c39d4fe31100 -r 871d8a5e0c67 Nominal/Perm.thy
--- a/Nominal/Perm.thy	Sun May 16 12:41:27 2010 +0100
+++ b/Nominal/Perm.thy	Mon May 17 12:00:54 2010 +0100
@@ -146,17 +146,20 @@
   val perms_zero_bind = Binding.name (perms_name ^ "_zero")
   val perms_plus_bind = Binding.name (perms_name ^ "_plus")
   
-  fun tac _ (_, simps, _) =
+  fun tac _ (_, _, simps) =
     Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
   
-  fun morphism phi (dfs, simps, fvs) =
-    (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs);
+  fun morphism phi (fvs, dfs, simps) =
+    (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps);
+
+  val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
 in
   lthy'
+  (*|> snd o (Local_Theory.note ((Binding.empty, [eqvt_attrib]), perm_eq_thms))*)
   |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))
   |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))
   |> Class_Target.prove_instantiation_exit_result morphism tac 
-       (perm_eq_thms, perm_zero_thms' @ perm_plus_thms', perm_funs)
+       (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms')
 end
 *}