--- a/Nominal/LFex.thy	Mon Mar 08 11:10:43 2010 +0100
+++ b/Nominal/LFex.thy	Mon Mar 08 11:12:15 2010 +0100
@@ -5,7 +5,7 @@
 atom_decl name
 atom_decl ident
 
-ML {* restricted_nominal := false *}
+ML {* restricted_nominal := 2 *}
 
 nominal_datatype kind =
     Type

--- a/Nominal/Parser.thy	Mon Mar 08 11:10:43 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 08 11:12:15 2010 +0100
@@ -223,7 +223,7 @@
 end
 *}
 
-ML {* val restricted_nominal=ref true *}
+ML {* val restricted_nominal=ref 0 *}
 
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
@@ -269,7 +269,7 @@
   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 then
+if !restricted_nominal = 0 then
   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
 else
 let
@@ -299,6 +299,11 @@
           typ_of_dtyp descr sorts (DtRec i))) l) descr);
   val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7;
   val (consts, const_defs) = split_list consts_defs;
+in
+if !restricted_nominal = 1 then
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy8)
+else
+let
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t]
       (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8;
@@ -341,6 +346,7 @@
   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20)
 end
 end
+end
 *}
 
 ML {*