--- a/Nominal/Parser.thy	Thu Mar 18 14:48:27 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 18 15:13:20 2010 +0100
@@ -379,16 +379,16 @@
   val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
   val lthy13 = Theory_Target.init NONE thy';
   val q_name = space_implode "_" qty_names;
+  fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
   val _ = tracing "Lifting induction";
   val constr_names = map (Long_Name.base_name o fst o dest_Const) consts;
   val q_induct = Rule_Cases.name constr_names (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"),
+    snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
+  val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
     [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names 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 (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
   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;
@@ -401,7 +401,7 @@
   val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2;
   val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_eq_iff_pre1
   val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_eq_iff_pre2
-  val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_eq_iff"), []), q_eq_iff) lthy17;
+  val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
   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;