--- a/src/Pure/simplifier.ML Mon Nov 11 20:00:53 2013 +0100
+++ b/src/Pure/simplifier.ML Mon Nov 11 20:50:12 2013 +0100
@@ -8,8 +8,6 @@
signature BASIC_SIMPLIFIER =
sig
include BASIC_RAW_SIMPLIFIER
- val Addsimprocs: simproc list -> unit
- val Delsimprocs: simproc list -> unit
val simp_tac: Proof.context -> int -> tactic
val asm_simp_tac: Proof.context -> int -> tactic
val full_simp_tac: Proof.context -> int -> tactic
@@ -126,16 +124,6 @@
val cong_del = attrib del_cong;
-(* global simprocs *)
-
-fun Addsimprocs args =
- Theory.setup (map_theory_simpset (fn ctxt => ctxt addsimprocs args));
-
-fun Delsimprocs args =
- Theory.setup (map_theory_simpset (fn ctxt => ctxt delsimprocs args));
-
-
-
(** named simprocs **)
structure Simprocs = Generic_Data
--- a/src/ZF/Datatype_ZF.thy Mon Nov 11 20:00:53 2013 +0100
+++ b/src/ZF/Datatype_ZF.thy Mon Nov 11 20:50:12 2013 +0100
@@ -107,9 +107,10 @@
val conv = Simplifier.simproc_global @{theory} "data_free" ["(x::i) = y"] proc;
end;
-
+*}
-Addsimprocs [DataFree.conv];
+setup {*
+ Simplifier.map_theory_simpset (fn ctxt => ctxt addsimprocs [DataFree.conv])
*}
end
--- a/src/ZF/arith_data.ML Mon Nov 11 20:00:53 2013 +0100
+++ b/src/ZF/arith_data.ML Mon Nov 11 20:50:12 2013 +0100
@@ -221,7 +221,9 @@
end;
-Addsimprocs ArithData.nat_cancel;
+val _ =
+ Theory.setup (Simplifier.map_theory_simpset (fn ctxt =>
+ ctxt addsimprocs ArithData.nat_cancel));
(*examples:
--- a/src/ZF/int_arith.ML Mon Nov 11 20:00:53 2013 +0100
+++ b/src/ZF/int_arith.ML Mon Nov 11 20:50:12 2013 +0100
@@ -320,10 +320,12 @@
end;
-
-Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
-Addsimprocs [Int_Numeral_Simprocs.combine_numerals,
- Int_Numeral_Simprocs.combine_numerals_prod];
+val _ =
+ Theory.setup (Simplifier.map_theory_simpset (fn ctxt =>
+ ctxt addsimprocs
+ (Int_Numeral_Simprocs.cancel_numerals @
+ [Int_Numeral_Simprocs.combine_numerals,
+ Int_Numeral_Simprocs.combine_numerals_prod])));
(*examples:*)