--- a/Nominal/Parser.thy	Tue Mar 16 20:07:13 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 17 08:39:46 2010 +0100
@@ -416,9 +416,11 @@
   val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_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 inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj
-  val q_inj_pre = map (lift_thm lthy17) inj_unfolded;
-  val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre
+  val inj_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_inj
+  val inj_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) inj_unfolded1
+  val q_inj_pre1 = map (lift_thm lthy17) inj_unfolded2;
+  val q_inj_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_inj_pre1
+  val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre2
   val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;
   val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
     (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))