--- a/Nominal/Parser.thy	Thu Mar 11 12:26:24 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 12:30:53 2010 +0100
@@ -374,7 +374,9 @@
   val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12;
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
   val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a;
-  val thy = Local_Theory.exit_global lthy12b;
+  val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
+  val (qbn_defs, lthy12c) = fold_map Quotient_Def.quotient_lift_const (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
+  val thy = Local_Theory.exit_global lthy12c;
   val perm_names = map (fn x => "permute_" ^ x) qty_names
   val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
   val lthy13 = Theory_Target.init NONE thy';