diff -r 8f5f7abe22c1 -r 632b08744613 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 11 12:30:53 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 13:34:45 2010 +0100
@@ -269,7 +269,6 @@
 end
 *}
 
-ML {* val restricted_nominal=ref 0 *}
 ML {* val cheat_alpha_eqvt = ref true *}
 ML {* val cheat_fv_eqvt = ref true *} (* Needed for non-rec *)
 ML {* val cheat_fv_rsp = ref true *}
@@ -380,11 +379,6 @@
   val perm_names = map (fn x => "permute_" ^ x) qty_names
   val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
   val lthy13 = Theory_Target.init NONE thy';
-in
-if !restricted_nominal = 0 then
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy13)
-else
-let
   val q_name = space_implode "_" qty_names;
   val q_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy13, induct));
   val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13;
@@ -408,7 +402,6 @@
 in
   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20)
 end
-end
 *}
 
 ML {*