--- a/src/Pure/simplifier.ML Wed Apr 10 17:17:16 2013 +0200
+++ b/src/Pure/simplifier.ML Wed Apr 10 17:27:38 2013 +0200
@@ -10,7 +10,6 @@
include BASIC_RAW_SIMPLIFIER
val map_simpset: (simpset -> simpset) -> Proof.context -> Proof.context
val simpset_of: Proof.context -> simpset
- val global_simpset_of: theory -> simpset
val Addsimprocs: simproc list -> unit
val Delsimprocs: simproc list -> unit
val simp_tac: simpset -> int -> tactic
@@ -169,8 +168,6 @@
(* global simpset *)
fun map_simpset_global f = Context.theory_map (map_ss f);
-fun global_simpset_of thy =
- Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy));
fun Addsimprocs args = Context.>> (map_ss (fn ss => ss addsimprocs args));
fun Delsimprocs args = Context.>> (map_ss (fn ss => ss delsimprocs args));