--- a/Nominal/NewAlpha.thy	Thu May 27 11:21:37 2010 +0200
+++ b/Nominal/NewAlpha.thy	Thu May 27 18:30:26 2010 +0200
@@ -206,7 +206,7 @@
 
   val (alphas, lthy') = Inductive.add_inductive_i
      {quiet_mode = true, verbose = false, alt_name = Binding.empty,
-      coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
+      coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
      all_alpha_names [] all_alpha_eqs [] lthy
 
   val alpha_ts_loc = #preds alphas;