1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Sep 05 17:12:40 2012 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Sep 05 19:51:00 2012 +0200
     1.3 @@ -527,7 +527,7 @@
     1.4        |> Sign.map_naming Name_Space.conceal
     1.5        |> Inductive.add_inductive_global
     1.6            {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
     1.7 -           coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
     1.8 +           coind = false, no_elim = true, no_ind = false, skip_mono = true}
     1.9            (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
    1.10               (rep_set_names' ~~ recTs'))
    1.11            [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
    1.12 @@ -1484,7 +1484,7 @@
    1.13        |> Sign.map_naming Name_Space.conceal
    1.14        |> Inductive.add_inductive_global
    1.15            {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
    1.16 -           coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
    1.17 +           coind = false, no_elim = false, no_ind = false, skip_mono = true}
    1.18            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    1.19            (map dest_Free rec_fns)
    1.20            (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []

     2.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Wed Sep 05 17:12:40 2012 +0200
     2.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Sep 05 19:51:00 2012 +0200
     2.3 @@ -178,7 +178,7 @@
     2.4        |> Sign.map_naming Name_Space.conceal
     2.5        |> Inductive.add_inductive_global
     2.6            {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
     2.7 -           coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
     2.8 +           coind = false, no_elim = true, no_ind = false, skip_mono = true}
     2.9            (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
    2.10            (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
    2.11        ||> Sign.restore_naming thy1

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

     4.1 --- a/src/HOL/Tools/Function/function_core.ML	Wed Sep 05 17:12:40 2012 +0200
     4.2 +++ b/src/HOL/Tools/Function/function_core.ML	Wed Sep 05 19:51:00 2012 +0200
     4.3 @@ -439,8 +439,7 @@
     4.4              coind = false,
     4.5              no_elim = false,
     4.6              no_ind = false,
     4.7 -            skip_mono = true,
     4.8 -            fork_mono = false}
     4.9 +            skip_mono = true}
    4.10            [binding] (* relation *)
    4.11            [] (* no parameters *)
    4.12            (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)

     5.1 --- a/src/HOL/Tools/inductive.ML	Wed Sep 05 17:12:40 2012 +0200
     5.2 +++ b/src/HOL/Tools/inductive.ML	Wed Sep 05 19:51:00 2012 +0200
     5.3 @@ -39,7 +39,7 @@
     5.4      thm list list * local_theory
     5.5    type inductive_flags =
     5.6      {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
     5.7 -      no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
     5.8 +      no_elim: bool, no_ind: bool, skip_mono: bool}
     5.9    val add_inductive_i:
    5.10      inductive_flags -> ((binding * typ) * mixfix) list ->
    5.11      (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
    5.12 @@ -358,10 +358,10 @@
    5.13  
    5.14  (* prove monotonicity *)
    5.15  
    5.16 -fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
    5.17 - (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
    5.18 +fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
    5.19 + (message (quiet_mode orelse skip_mono andalso ! quick_and_dirty)
    5.20      "  Proving monotonicity ...";
    5.21 -  (if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
    5.22 +  (if skip_mono then Skip_Proof.prove else Goal.prove_future) ctxt
    5.23      [] []
    5.24      (HOLogic.mk_Trueprop
    5.25        (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
    5.26 @@ -746,8 +746,7 @@
    5.27  
    5.28  (** specification of (co)inductive predicates **)
    5.29  
    5.30 -fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind
    5.31 -    cs intr_ts monos params cnames_syn lthy =
    5.32 +fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn lthy =
    5.33    let
    5.34      val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
    5.35  
    5.36 @@ -841,7 +840,7 @@
    5.37      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
    5.38  
    5.39      val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
    5.40 -    val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy''';
    5.41 +    val mono = prove_mono quiet_mode skip_mono predT fp_fun monos lthy''';
    5.42      val (_, lthy'''') =
    5.43        Local_Theory.note (apfst Binding.conceal Attrib.empty_binding,
    5.44          Proof_Context.export lthy''' lthy'' [mono]) lthy'';
    5.45 @@ -912,7 +911,7 @@
    5.46  
    5.47  type inductive_flags =
    5.48    {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
    5.49 -    no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool};
    5.50 +    no_elim: bool, no_ind: bool, skip_mono: bool};
    5.51  
    5.52  type add_ind_def =
    5.53    inductive_flags ->
    5.54 @@ -920,7 +919,7 @@
    5.55    term list -> (binding * mixfix) list ->
    5.56    local_theory -> inductive_result * local_theory;
    5.57  
    5.58 -fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
    5.59 +fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono}
    5.60      cs intros monos params cnames_syn lthy =
    5.61    let
    5.62      val _ = null cnames_syn andalso error "No inductive predicates given";
    5.63 @@ -933,7 +932,7 @@
    5.64        apfst split_list (split_list (map (check_rule lthy cs params) intros));
    5.65  
    5.66      val (lthy1, lthy2, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
    5.67 -      argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts
    5.68 +      argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts
    5.69          monos params cnames_syn lthy;
    5.70  
    5.71      val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
    5.72 @@ -983,7 +982,7 @@
    5.73  (* external interfaces *)
    5.74  
    5.75  fun gen_add_inductive_i mk_def
    5.76 -    (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
    5.77 +    (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono})
    5.78      cnames_syn pnames spec monos lthy =
    5.79    let
    5.80      val thy = Proof_Context.theory_of lthy;
    5.81 @@ -1047,8 +1046,9 @@
    5.82        |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
    5.83      val (cs, ps) = chop (length cnames_syn) vars;
    5.84      val monos = Attrib.eval_thms lthy raw_monos;
    5.85 -    val flags = {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
    5.86 -      coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int};
    5.87 +    val flags =
    5.88 +     {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
    5.89 +      coind = coind, no_elim = false, no_ind = false, skip_mono = false};
    5.90    in
    5.91      lthy
    5.92      |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos

     6.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Sep 05 17:12:40 2012 +0200
     6.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Sep 05 19:51:00 2012 +0200
     6.3 @@ -355,7 +355,7 @@
     6.4      val (ind_info, thy3') = thy2 |>
     6.5        Inductive.add_inductive_global
     6.6          {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
     6.7 -          no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
     6.8 +          no_elim = false, no_ind = false, skip_mono = false}
     6.9          rlzpreds rlzparams (map (fn (rintr, intr) =>
    6.10            ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
    6.11             subst_atomic rlzpreds' (Logic.unvarify_global rintr)))

     7.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Sep 05 17:12:40 2012 +0200
     7.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Sep 05 19:51:00 2012 +0200
     7.3 @@ -417,7 +417,7 @@
     7.4  (**** definition of inductive sets ****)
     7.5  
     7.6  fun add_ind_set_def
     7.7 -    {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
     7.8 +    {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono}
     7.9      cs intros monos params cnames_syn lthy =
    7.10    let
    7.11      val thy = Proof_Context.theory_of lthy;
    7.12 @@ -490,8 +490,7 @@
    7.13      val ({preds, intrs, elims, raw_induct, eqs, ...}, lthy1) =
    7.14        Inductive.add_ind_def
    7.15          {quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty,
    7.16 -          coind = coind, no_elim = no_elim, no_ind = no_ind,
    7.17 -          skip_mono = skip_mono, fork_mono = fork_mono}
    7.18 +          coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
    7.19          cs' intros' monos' params1 cnames_syn' lthy;
    7.20  
    7.21      (* define inductive sets using previously defined predicates *)