# HG changeset patch
# User wenzelm
# Date 1384199412 -3600
# Node ID 8b165615ffe3b1a126633e542168d0a581674d4c
# Parent  890e983cb07bd3b8980cdc99e741b8652999b63e
tuned signature -- removed obsolete Addsimprocs, Delsimprocs;

diff -r 890e983cb07b -r 8b165615ffe3 src/Pure/simplifier.ML
--- 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
diff -r 890e983cb07b -r 8b165615ffe3 src/ZF/Datatype_ZF.thy
--- 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
diff -r 890e983cb07b -r 8b165615ffe3 src/ZF/arith_data.ML
--- 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:
diff -r 890e983cb07b -r 8b165615ffe3 src/ZF/int_arith.ML
--- 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:*)