--- a/Nominal/Parser.thy	Tue Mar 09 11:36:40 2010 +0100
+++ b/Nominal/Parser.thy	Tue Mar 09 16:24:39 2010 +0100
@@ -146,7 +146,7 @@
 ML {* 
 fun rawify_binds dts_env cnstrs_env bn_fun_env binds =
   map (map (map (map (fn (opt_trm, i, j) => 
-    (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env) opt_trm, i, j))))) binds
+    (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j))))) binds
 *}
 
 ML {* 
@@ -232,6 +232,8 @@
   val thy_name = Context.theory_name thy
   val (((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), 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_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc
   val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
@@ -250,7 +252,12 @@
   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
     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 lthy3;
+  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;
@@ -268,11 +275,6 @@
   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), lthy4)
-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;
@@ -436,7 +438,7 @@
   fun prep_bn env bn_str =
     case (Syntax.read_term lthy bn_str) of
        Free (x, _) => (NONE, env_lookup env x)
-     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), env_lookup env x)
+     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), true), env_lookup env x)
      | _ => error (bn_str ^ " not allowed as binding specification.");  
  
   fun prep_typ env (i, opt_name) =