--- a/Nominal/Parser.thy	Thu Mar 18 11:37:10 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 18 12:09:59 2010 +0100
@@ -381,15 +381,18 @@
   val q_name = space_implode "_" qty_names;
   val _ = tracing "Lifting induction";
   val q_induct = lift_thm lthy13 induct;
+  fun note_simp_suffix s th ctxt =
+    snd (Local_Theory.note ((Binding.name (q_name ^ "_" ^ s),
+      [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
   val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13;
   val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct
   val (_, lthy14a) = Local_Theory.note ((Binding.name (q_name ^ "_inducts"), []), q_inducts) lthy14;
-  val q_perm = map (lift_thm lthy14) raw_perm_def;
-  val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14a;
+  val q_perm = map (lift_thm lthy14) raw_perm_def; 
+  val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
   val q_fv = map (lift_thm lthy15) fv_def;
-  val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
+  val lthy16 = note_simp_suffix "fv" q_fv lthy15;
   val q_bn = map (lift_thm lthy16) raw_bn_eqs;
-  val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
+  val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = tracing "Lifting eq-iff";
   val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_eq_iff
   val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) eq_iff_unfolded1
@@ -400,7 +403,7 @@
   val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
     (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))
   val q_dis = map (lift_thm lthy18) rel_dists;
-  val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18;
+  val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
   val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt;
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;