--- a/Nominal/Parser.thy	Sun Mar 07 21:30:57 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 08 15:01:01 2010 +0100
@@ -326,9 +326,9 @@
   val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
   val q_bn = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs;
   val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
-  val inj_unfolded = map (LocalDefs.unfold lthy17 @{thms alpha_gen}) alpha_inj
+  val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj
   val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded;
-  val q_inj = map (LocalDefs.fold lthy17 @{thms alpha_gen}) q_inj_pre
+  val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre
   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)))))