--- a/Nominal/NewParser.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/NewParser.thy	Tue May 11 18:20:25 2010 +0200
@@ -395,7 +395,10 @@
   val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
   val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
-  val thy = Local_Theory.exit_global lthy2;
+
+  val (_, lthy2a) = Local_Theory.note ((Binding.empty,
+    [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2;
+  val thy = Local_Theory.exit_global lthy2a;
   val thy_name = Context.theory_name thy
 
   val lthy3 = Theory_Target.init NONE thy;