--- a/Nominal/Perm.thy	Mon May 17 12:00:54 2010 +0100
+++ b/Nominal/Perm.thy	Mon May 17 12:46:51 2010 +0100
@@ -151,11 +151,8 @@
   
   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 
@@ -169,6 +166,8 @@
 
 (* permutations for quotient types *)
 
+ML {* Class_Target.prove_instantiation_exit_result *}
+
 ML {*
 fun quotient_lift_consts_export qtys spec ctxt =
 let