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