--- a/src/HOL/Nominal/nominal_datatype.ML Wed Sep 05 17:12:40 2012 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Sep 05 19:51:00 2012 +0200
@@ -527,7 +527,7 @@
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global
{quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_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, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
(rep_set_names' ~~ recTs'))
[] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
@@ -1484,7 +1484,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 = false, skip_mono = true, fork_mono = false}
+ coind = false, no_elim = false, no_ind = false, 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) []