# HG changeset patch
# User wenzelm
# Date 1346867460 -7200
# Node ID 03bee3a6a1b7bcf9eb0c747b6708c48170b46e5d
# Parent  bde6d900b42ad37884ff7c18085512836b817696
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;

diff -r bde6d900b42a -r 03bee3a6a1b7 src/HOL/Nominal/nominal_datatype.ML
--- 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) []
diff -r bde6d900b42a -r 03bee3a6a1b7 src/HOL/Tools/Datatype/datatype.ML
--- 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
diff -r bde6d900b42a -r 03bee3a6a1b7 src/HOL/Tools/Datatype/rep_datatype.ML
--- 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) []
diff -r bde6d900b42a -r 03bee3a6a1b7 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Wed Sep 05 17:12:40 2012 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Wed Sep 05 19:51:00 2012 +0200
@@ -439,8 +439,7 @@
             coind = false,
             no_elim = false,
             no_ind = false,
-            skip_mono = true,
-            fork_mono = false}
+            skip_mono = true}
           [binding] (* relation *)
           [] (* no parameters *)
           (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
diff -r bde6d900b42a -r 03bee3a6a1b7 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Sep 05 17:12:40 2012 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Sep 05 19:51:00 2012 +0200
@@ -39,7 +39,7 @@
     thm list list * local_theory
   type inductive_flags =
     {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
-      no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
+      no_elim: bool, no_ind: bool, skip_mono: bool}
   val add_inductive_i:
     inductive_flags -> ((binding * typ) * mixfix) list ->
     (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
@@ -358,10 +358,10 @@
 
 (* prove monotonicity *)
 
-fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
- (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
+fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
+ (message (quiet_mode orelse skip_mono andalso ! quick_and_dirty)
     "  Proving monotonicity ...";
-  (if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
+  (if skip_mono then Skip_Proof.prove else Goal.prove_future) ctxt
     [] []
     (HOLogic.mk_Trueprop
       (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
@@ -746,8 +746,7 @@
 
 (** specification of (co)inductive predicates **)
 
-fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind
-    cs intr_ts monos params cnames_syn lthy =
+fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn lthy =
   let
     val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
 
@@ -841,7 +840,7 @@
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
     val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
-    val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy''';
+    val mono = prove_mono quiet_mode skip_mono predT fp_fun monos lthy''';
     val (_, lthy'''') =
       Local_Theory.note (apfst Binding.conceal Attrib.empty_binding,
         Proof_Context.export lthy''' lthy'' [mono]) lthy'';
@@ -912,7 +911,7 @@
 
 type inductive_flags =
   {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
-    no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool};
+    no_elim: bool, no_ind: bool, skip_mono: bool};
 
 type add_ind_def =
   inductive_flags ->
@@ -920,7 +919,7 @@
   term list -> (binding * mixfix) list ->
   local_theory -> inductive_result * local_theory;
 
-fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
+fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono}
     cs intros monos params cnames_syn lthy =
   let
     val _ = null cnames_syn andalso error "No inductive predicates given";
@@ -933,7 +932,7 @@
       apfst split_list (split_list (map (check_rule lthy cs params) intros));
 
     val (lthy1, lthy2, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
-      argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts
+      argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts
         monos params cnames_syn lthy;
 
     val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
@@ -983,7 +982,7 @@
 (* external interfaces *)
 
 fun gen_add_inductive_i mk_def
-    (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
+    (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono})
     cnames_syn pnames spec monos lthy =
   let
     val thy = Proof_Context.theory_of lthy;
@@ -1047,8 +1046,9 @@
       |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
     val (cs, ps) = chop (length cnames_syn) vars;
     val monos = Attrib.eval_thms lthy raw_monos;
-    val flags = {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
-      coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int};
+    val flags =
+     {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
+      coind = coind, no_elim = false, no_ind = false, skip_mono = false};
   in
     lthy
     |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos
diff -r bde6d900b42a -r 03bee3a6a1b7 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Sep 05 17:12:40 2012 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Sep 05 19:51:00 2012 +0200
@@ -355,7 +355,7 @@
     val (ind_info, thy3') = thy2 |>
       Inductive.add_inductive_global
         {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
-          no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
+          no_elim = false, no_ind = false, skip_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
           ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
            subst_atomic rlzpreds' (Logic.unvarify_global rintr)))
diff -r bde6d900b42a -r 03bee3a6a1b7 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Wed Sep 05 17:12:40 2012 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Wed Sep 05 19:51:00 2012 +0200
@@ -417,7 +417,7 @@
 (**** definition of inductive sets ****)
 
 fun add_ind_set_def
-    {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
+    {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono}
     cs intros monos params cnames_syn lthy =
   let
     val thy = Proof_Context.theory_of lthy;
@@ -490,8 +490,7 @@
     val ({preds, intrs, elims, raw_induct, eqs, ...}, lthy1) =
       Inductive.add_ind_def
         {quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty,
-          coind = coind, no_elim = no_elim, no_ind = no_ind,
-          skip_mono = skip_mono, fork_mono = fork_mono}
+          coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
         cs' intros' monos' params1 cnames_syn' lthy;
 
     (* define inductive sets using previously defined predicates *)