eliminated unused arith "verbose" flag -- tools that need options can use the context;
authorwenzelm
Mon Mar 09 11:32:32 2015 +0100 (2015-03-09)
changeset 596572441a80fb6c1
parent 59656 ddc5411c1cb9
child 59658 0cc388370041
child 59660 49e498cedd02
eliminated unused arith "verbose" flag -- tools that need options can use the context;
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Mar 09 11:21:00 2015 +0100
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Mar 09 11:32:32 2015 +0100
     1.3 @@ -907,7 +907,7 @@
     1.4      (Attrib.setup @{binding presburger}
     1.5        ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
     1.6          optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm"
     1.7 -    #> Arith_Data.add_tactic "Presburger arithmetic" (K (tac true [] [])));
     1.8 +    #> Arith_Data.add_tactic "Presburger arithmetic" (tac true [] []));
     1.9  
    1.10  end;
    1.11  
     2.1 --- a/src/HOL/Tools/arith_data.ML	Mon Mar 09 11:21:00 2015 +0100
     2.2 +++ b/src/HOL/Tools/arith_data.ML	Mon Mar 09 11:32:32 2015 +0100
     2.3 @@ -7,8 +7,7 @@
     2.4  signature ARITH_DATA =
     2.5  sig
     2.6    val arith_tac: Proof.context -> int -> tactic
     2.7 -  val verbose_arith_tac: Proof.context -> int -> tactic
     2.8 -  val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory
     2.9 +  val add_tactic: string -> (Proof.context -> int -> tactic) -> theory -> theory
    2.10  
    2.11    val mk_number: typ -> int -> term
    2.12    val mk_sum: typ -> term list -> term
    2.13 @@ -29,7 +28,7 @@
    2.14  
    2.15  structure Arith_Tactics = Theory_Data
    2.16  (
    2.17 -  type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
    2.18 +  type T = (serial * (string * (Proof.context -> int -> tactic))) list;
    2.19    val empty = [];
    2.20    val extend = I;
    2.21    fun merge data : T = AList.merge (op =) (K true) data;
    2.22 @@ -37,15 +36,12 @@
    2.23  
    2.24  fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
    2.25  
    2.26 -fun gen_arith_tac verbose ctxt =
    2.27 +fun arith_tac ctxt =
    2.28    let
    2.29      val tactics = Arith_Tactics.get (Proof_Context.theory_of ctxt);
    2.30 -    fun invoke (_, (_, tac)) k st = tac verbose ctxt k st;
    2.31 +    fun invoke (_, (_, tac)) k st = tac ctxt k st;
    2.32    in FIRST' (map invoke (rev tactics)) end;
    2.33  
    2.34 -val arith_tac = gen_arith_tac false;
    2.35 -val verbose_arith_tac = gen_arith_tac true;
    2.36 -
    2.37  val _ =
    2.38    Theory.setup
    2.39      (Method.setup @{binding arith}
    2.40 @@ -53,7 +49,7 @@
    2.41          METHOD (fn facts =>
    2.42            HEADGOAL
    2.43            (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
    2.44 -            THEN' verbose_arith_tac ctxt))))
    2.45 +            THEN' arith_tac ctxt))))
    2.46        "various arithmetic decision procedures");
    2.47  
    2.48  
     3.1 --- a/src/HOL/Tools/lin_arith.ML	Mon Mar 09 11:21:00 2015 +0100
     3.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon Mar 09 11:32:32 2015 +0100
     3.3 @@ -892,7 +892,7 @@
     3.4        METHOD (fn facts =>
     3.5          HEADGOAL (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
     3.6            THEN' tac ctxt)))) "linear arithmetic" #>
     3.7 -  Arith_Data.add_tactic "linear arithmetic" (K tac);
     3.8 +  Arith_Data.add_tactic "linear arithmetic" tac;
     3.9  
    3.10  val setup =
    3.11    init_arith_data
     4.1 --- a/src/HOL/Word/Word.thy	Mon Mar 09 11:21:00 2015 +0100
     4.2 +++ b/src/HOL/Word/Word.thy	Mon Mar 09 11:32:32 2015 +0100
     4.3 @@ -1551,7 +1551,7 @@
     4.4  fun uint_arith_tacs ctxt = 
     4.5    let
     4.6      fun arith_tac' n t =
     4.7 -      Arith_Data.verbose_arith_tac ctxt n t
     4.8 +      Arith_Data.arith_tac ctxt n t
     4.9          handle Cooper.COOPER _ => Seq.empty;
    4.10    in 
    4.11      [ clarify_tac ctxt 1,
    4.12 @@ -2053,7 +2053,7 @@
    4.13  fun unat_arith_tacs ctxt =   
    4.14    let
    4.15      fun arith_tac' n t =
    4.16 -      Arith_Data.verbose_arith_tac ctxt n t
    4.17 +      Arith_Data.arith_tac ctxt n t
    4.18          handle Cooper.COOPER _ => Seq.empty;
    4.19    in 
    4.20      [ clarify_tac ctxt 1,