diff -r 93e7c1d8cc5c -r 995d47b09ab4 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Tue Aug 28 16:48:07 2012 +0100 +++ b/Nominal/nominal_dt_alpha.ML Thu Oct 04 11:10:23 2012 +0100 @@ -250,7 +250,7 @@ val (alpha_info, lthy') = Inductive.add_inductive_i {quiet_mode = true, verbose = false, alt_name = Binding.empty, - coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} + coind = false, no_elim = false, no_ind = false, skip_mono = false} all_alpha_names [] all_alpha_intros [] lthy val all_alpha_trms_loc = #preds alpha_info;