diff -r f00761b5957e -r 226693549aa0 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Mon Mar 08 15:01:01 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 08 15:01:26 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 {*