--- a/src/HOL/Tools/Datatype/datatype.ML Wed Sep 05 17:12:40 2012 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Wed Sep 05 19:51:00 2012 +0200
@@ -178,7 +178,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 = true, no_ind = false, skip_mono = true, fork_mono = false}
+ coind = false, no_elim = true, no_ind = false, skip_mono = true}
(map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
(map (fn x => (Attrib.empty_binding, x)) intr_ts) []
||> Sign.restore_naming thy1