# HG changeset patch
# User wenzelm
# Date 1365607658 -7200
# Node ID 27ecd33d3366943ef450bc9210d5fff97e062667
# Parent  3d8720271ebf614dee6f5125f1e60a28b685f173
obsolete -- tools should refer to proper Proof.context;

diff -r 3d8720271ebf -r 27ecd33d3366 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Apr 10 17:17:16 2013 +0200
+++ b/src/Provers/classical.ML	Wed Apr 10 17:27:38 2013 +0200
@@ -56,7 +56,6 @@
   val appSWrappers: Proof.context -> wrapper
   val appWrappers: Proof.context -> wrapper
 
-  val global_claset_of: theory -> claset
   val claset_of: Proof.context -> claset
   val map_claset: (claset -> claset) -> Proof.context -> Proof.context
   val put_claset: claset -> Proof.context -> Proof.context
@@ -596,7 +595,6 @@
   val merge = merge_cs;
 );
 
-val global_claset_of = Claset.get o Context.Theory;
 val claset_of = Claset.get o Context.Proof;
 val rep_claset_of = rep_cs o claset_of;
 
diff -r 3d8720271ebf -r 27ecd33d3366 src/Pure/simplifier.ML
--- 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));