diff -r 0c1dcdefb515 -r 31f1ec832d39 Nominal/NewAlpha.thy --- 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;