--- a/src/HOL/Tools/Datatype/rep_datatype.ML Wed Sep 05 17:12:40 2012 +0200
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Wed Sep 05 19:51:00 2012 +0200
@@ -145,7 +145,7 @@
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global
{quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
- coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false}
+ coind = false, no_elim = false, no_ind = true, skip_mono = true}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
(map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []