eliminated dead code;
authorwenzelm
Fri Oct 02 23:15:36 2009 +0200 (2009-10-02 ago)
changeset 328635e8cef567042
parent 32862 1fc86cec3bdf
child 32865 f8d1e16ec758
child 32866 1238cbb7c08f
eliminated dead code;
tuned;
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/old_primrec.ML
src/HOL/Tools/recdef.ML
src/Provers/classical.ML
src/Tools/induct_tacs.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Oct 02 22:15:30 2009 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Oct 02 23:15:36 2009 +0200
     1.3 @@ -95,7 +95,6 @@
     1.4  );
     1.5  
     1.6  fun lookup_thread xs = AList.lookup Thread.equal xs;
     1.7 -fun delete_thread xs = AList.delete Thread.equal xs;
     1.8  fun update_thread xs = AList.update Thread.equal xs;
     1.9  
    1.10  
    1.11 @@ -121,7 +120,8 @@
    1.12  (* unregister thread *)
    1.13  
    1.14  fun unregister (success, message) thread = Synchronized.change state
    1.15 -  (fn state as State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
    1.16 +  (fn state as
    1.17 +      State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
    1.18      (case lookup_thread active thread of
    1.19        SOME (birthtime, _, description) =>
    1.20          let
    1.21 @@ -326,9 +326,11 @@
    1.22  fun print_provers thy = Pretty.writeln
    1.23    (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
    1.24  
    1.25 -fun get_prover name thy = case Symtab.lookup (Provers.get thy) name of
    1.26 -  NONE => NONE
    1.27 -| SOME (prover, _) => SOME prover;
    1.28 +fun get_prover name thy =
    1.29 +  (case Symtab.lookup (Provers.get thy) name of
    1.30 +    NONE => NONE
    1.31 +  | SOME (prover, _) => SOME prover);
    1.32 +
    1.33  
    1.34  (* start prover thread *)
    1.35  
     2.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Oct 02 22:15:30 2009 +0200
     2.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Oct 02 23:15:36 2009 +0200
     2.3 @@ -767,8 +767,6 @@
     2.4  
     2.5  structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data);
     2.6  
     2.7 -val map_data = Fast_Arith.map_data;
     2.8 -
     2.9  fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
    2.10    {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
    2.11      lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of};
     3.1 --- a/src/HOL/Tools/old_primrec.ML	Fri Oct 02 22:15:30 2009 +0200
     3.2 +++ b/src/HOL/Tools/old_primrec.ML	Fri Oct 02 23:15:36 2009 +0200
     3.3 @@ -318,31 +318,7 @@
     3.4  val add_primrec_unchecked = gen_primrec thy_note (thy_def true);
     3.5  val add_primrec_i = gen_primrec_i thy_note (thy_def false);
     3.6  val add_primrec_unchecked_i = gen_primrec_i thy_note (thy_def true);
     3.7 -fun gen_primrec note def alt_name specs =
     3.8 -  gen_primrec_i note def alt_name (map (fn ((name, t), atts) => ((name, atts), t)) specs);
     3.9  
    3.10  end;
    3.11  
    3.12 -
    3.13 -(* see primrec.ML (* outer syntax *)
    3.14 -
    3.15 -local structure P = OuterParse and K = OuterKeyword in
    3.16 -
    3.17 -val opt_unchecked_name =
    3.18 -  Scan.optional (P.$$$ "(" |-- P.!!!
    3.19 -    (((P.$$$ "unchecked" >> K true) -- Scan.optional P.name "" ||
    3.20 -      P.name >> pair false) --| P.$$$ ")")) (false, "");
    3.21 -
    3.22 -val primrec_decl =
    3.23 -  opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
    3.24 -
    3.25 -val _ =
    3.26 -  OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
    3.27 -    (primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
    3.28 -      Toplevel.theory (snd o
    3.29 -        (if unchecked then add_primrec_unchecked else add_primrec) alt_name
    3.30 -          (map P.triple_swap eqns))));
    3.31 -
    3.32 -end;*)
    3.33 -
    3.34  end;
     4.1 --- a/src/HOL/Tools/recdef.ML	Fri Oct 02 22:15:30 2009 +0200
     4.2 +++ b/src/HOL/Tools/recdef.ML	Fri Oct 02 23:15:36 2009 +0200
     4.3 @@ -47,11 +47,6 @@
     4.4  fun map_congs f = map_hints (fn (simps, congs, wfs) => (simps, f congs, wfs));
     4.5  fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs));
     4.6  
     4.7 -fun pretty_hints ({simps, congs, wfs}: hints) =
     4.8 - [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm_without_context simps),
     4.9 -  Pretty.big_list "recdef cong hints:" (map Display.pretty_thm_without_context (map snd congs)),
    4.10 -  Pretty.big_list "recdef wf hints:" (map Display.pretty_thm_without_context wfs)];
    4.11 -
    4.12  
    4.13  (* congruence rules *)
    4.14  
     5.1 --- a/src/Provers/classical.ML	Fri Oct 02 22:15:30 2009 +0200
     5.2 +++ b/src/Provers/classical.ML	Fri Oct 02 23:15:36 2009 +0200
     5.3 @@ -768,7 +768,7 @@
     5.4  (*Non-deterministic!  Could always expand the first unsafe connective.
     5.5    That's hard to implement and did not perform better in experiments, due to
     5.6    greater search depth required.*)
     5.7 -fun dup_step_tac (cs as (CS{dup_netpair,...})) =
     5.8 +fun dup_step_tac (CS {dup_netpair, ...}) =
     5.9    biresolve_from_nets_tac dup_netpair;
    5.10  
    5.11  (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
     6.1 --- a/src/Tools/induct_tacs.ML	Fri Oct 02 22:15:30 2009 +0200
     6.2 +++ b/src/Tools/induct_tacs.ML	Fri Oct 02 23:15:36 2009 +0200
     6.3 @@ -28,7 +28,7 @@
     6.4  
     6.5  fun gen_case_tac ctxt0 s opt_rule i st =
     6.6    let
     6.7 -    val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
     6.8 +    val (_, ctxt) = Variable.focus_subgoal i st ctxt0;
     6.9      val rule =
    6.10        (case opt_rule of
    6.11          SOME rule => rule