--- a/Nominal/Parser.thy	Wed Mar 10 16:50:42 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 10 16:51:15 2010 +0100
@@ -278,9 +278,10 @@
   val thy_name = Context.theory_name thy
   val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) =
     raw_nominal_decls dts bn_funs bn_eqs binds lthy
-  val bn_funs_decls = [];
+  val morphism_2_1 = ProofContext.export_morphism lthy2 lthy
+  val raw_bns_exp = map (apsnd (map (apfst (Morphism.term morphism_2_1)))) raw_bns;
+  val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
 
-  val morphism_2_1 = ProofContext.export_morphism lthy2 lthy
   val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc
   val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names);
@@ -299,11 +300,6 @@
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
   val raw_binds_flat = map (map flat) raw_binds;
   val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3;
-in
-if !restricted_nominal = 0 then
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
-else
-let
   val alpha_ts_loc = #preds alpha
   val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
   val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc;
@@ -321,6 +317,11 @@
   val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
   val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
+in
+if !restricted_nominal = 0 then
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy5)
+else
+let
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms
     ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5;