--- a/Nominal/NewParser.thy	Mon May 17 12:00:54 2010 +0100
+++ b/Nominal/NewParser.thy	Mon May 17 12:46:51 2010 +0100
@@ -394,9 +394,10 @@
     if get_STEPS lthy1 > 2 
     then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
     else raise TEST lthy1
-
-  val (_, lthy2a) = Local_Theory.note ((Binding.empty,
-    [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_defs) lthy2;
+ 
+  (* noting the raw permutations as eqvt theorems *)
+  val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
+  val (_, lthy2a) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_defs) lthy2
 
   val thy = Local_Theory.exit_global lthy2a;
   val thy_name = Context.theory_name thy

--- 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