diff -r 10eca65a8d03 -r 6f346b649f8e Nominal/Parser.thy
--- a/Nominal/Parser.thy	Wed Mar 10 15:32:51 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 10 15:34:13 2010 +0100
@@ -317,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;
@@ -325,11 +330,6 @@
   val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms
     (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6;
   val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
-in
-if !restricted_nominal = 0 then
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy5)
-else
-let
   val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc
   val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
     inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;