tuned signature -- removed obsolete Addsimprocs, Delsimprocs;
authorwenzelm
Mon Nov 11 20:50:12 2013 +0100 (2013-11-11)
changeset 543888b165615ffe3
parent 54387 890e983cb07b
child 54389 a4051679a7bf
tuned signature -- removed obsolete Addsimprocs, Delsimprocs;
src/Pure/simplifier.ML
src/ZF/Datatype_ZF.thy
src/ZF/arith_data.ML
src/ZF/int_arith.ML
     1.1 --- a/src/Pure/simplifier.ML	Mon Nov 11 20:00:53 2013 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Mon Nov 11 20:50:12 2013 +0100
     1.3 @@ -8,8 +8,6 @@
     1.4  signature BASIC_SIMPLIFIER =
     1.5  sig
     1.6    include BASIC_RAW_SIMPLIFIER
     1.7 -  val Addsimprocs: simproc list -> unit
     1.8 -  val Delsimprocs: simproc list -> unit
     1.9    val simp_tac: Proof.context -> int -> tactic
    1.10    val asm_simp_tac: Proof.context -> int -> tactic
    1.11    val full_simp_tac: Proof.context -> int -> tactic
    1.12 @@ -126,16 +124,6 @@
    1.13  val cong_del = attrib del_cong;
    1.14  
    1.15  
    1.16 -(* global simprocs *)
    1.17 -
    1.18 -fun Addsimprocs args =
    1.19 -  Theory.setup (map_theory_simpset (fn ctxt => ctxt addsimprocs args));
    1.20 -
    1.21 -fun Delsimprocs args =
    1.22 -  Theory.setup (map_theory_simpset (fn ctxt => ctxt delsimprocs args));
    1.23 -
    1.24 -
    1.25 -
    1.26  (** named simprocs **)
    1.27  
    1.28  structure Simprocs = Generic_Data
     2.1 --- a/src/ZF/Datatype_ZF.thy	Mon Nov 11 20:00:53 2013 +0100
     2.2 +++ b/src/ZF/Datatype_ZF.thy	Mon Nov 11 20:50:12 2013 +0100
     2.3 @@ -107,9 +107,10 @@
     2.4   val conv = Simplifier.simproc_global @{theory} "data_free" ["(x::i) = y"] proc;
     2.5  
     2.6  end;
     2.7 -
     2.8 +*}
     2.9  
    2.10 -Addsimprocs [DataFree.conv];
    2.11 +setup {*
    2.12 +  Simplifier.map_theory_simpset (fn ctxt => ctxt addsimprocs [DataFree.conv])
    2.13  *}
    2.14  
    2.15  end
     3.1 --- a/src/ZF/arith_data.ML	Mon Nov 11 20:00:53 2013 +0100
     3.2 +++ b/src/ZF/arith_data.ML	Mon Nov 11 20:50:12 2013 +0100
     3.3 @@ -221,7 +221,9 @@
     3.4  
     3.5  end;
     3.6  
     3.7 -Addsimprocs ArithData.nat_cancel;
     3.8 +val _ =
     3.9 +  Theory.setup (Simplifier.map_theory_simpset (fn ctxt =>
    3.10 +    ctxt addsimprocs ArithData.nat_cancel));
    3.11  
    3.12  
    3.13  (*examples:
     4.1 --- a/src/ZF/int_arith.ML	Mon Nov 11 20:00:53 2013 +0100
     4.2 +++ b/src/ZF/int_arith.ML	Mon Nov 11 20:50:12 2013 +0100
     4.3 @@ -320,10 +320,12 @@
     4.4  
     4.5  end;
     4.6  
     4.7 -
     4.8 -Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
     4.9 -Addsimprocs [Int_Numeral_Simprocs.combine_numerals,
    4.10 -             Int_Numeral_Simprocs.combine_numerals_prod];
    4.11 +val _ =
    4.12 +  Theory.setup (Simplifier.map_theory_simpset (fn ctxt =>
    4.13 +    ctxt addsimprocs
    4.14 +      (Int_Numeral_Simprocs.cancel_numerals @
    4.15 +       [Int_Numeral_Simprocs.combine_numerals,
    4.16 +        Int_Numeral_Simprocs.combine_numerals_prod])));
    4.17  
    4.18  
    4.19  (*examples:*)