--- a/src/Pure/raw_simplifier.ML Wed Jan 01 13:24:23 2014 +0100
+++ b/src/Pure/raw_simplifier.ML Wed Jan 01 14:29:22 2014 +0100
@@ -40,7 +40,6 @@
val mk_simproc: string -> cterm list -> (Proof.context -> term -> thm option) -> simproc
val simpset_of: Proof.context -> simpset
val put_simpset: simpset -> Proof.context -> Proof.context
- val global_context: theory -> simpset -> Proof.context
val simpset_map: Proof.context -> (Proof.context -> Proof.context) -> simpset -> simpset
val map_theory_simpset: (Proof.context -> Proof.context) -> theory -> theory
val empty_simpset: Proof.context -> Proof.context
@@ -388,8 +387,6 @@
val Simpset ({bounds, depth, ...}, _) = context_ss;
in Simpset (make_ss1 (rules, prems, bounds, depth), ss2) end);
-fun global_context thy ss = Proof_Context.init_global thy |> put_simpset ss;
-
val empty_simpset = put_simpset empty_ss;
fun map_theory_simpset f thy =