obsolete -- tools should refer to proper Proof.context;
authorwenzelm
Wed Apr 10 17:27:38 2013 +0200 (2013-04-10)
changeset 5168827ecd33d3366
parent 51687 3d8720271ebf
child 51689 43a3465805dd
obsolete -- tools should refer to proper Proof.context;
src/Provers/classical.ML
src/Pure/simplifier.ML
     1.1 --- a/src/Provers/classical.ML	Wed Apr 10 17:17:16 2013 +0200
     1.2 +++ b/src/Provers/classical.ML	Wed Apr 10 17:27:38 2013 +0200
     1.3 @@ -56,7 +56,6 @@
     1.4    val appSWrappers: Proof.context -> wrapper
     1.5    val appWrappers: Proof.context -> wrapper
     1.6  
     1.7 -  val global_claset_of: theory -> claset
     1.8    val claset_of: Proof.context -> claset
     1.9    val map_claset: (claset -> claset) -> Proof.context -> Proof.context
    1.10    val put_claset: claset -> Proof.context -> Proof.context
    1.11 @@ -596,7 +595,6 @@
    1.12    val merge = merge_cs;
    1.13  );
    1.14  
    1.15 -val global_claset_of = Claset.get o Context.Theory;
    1.16  val claset_of = Claset.get o Context.Proof;
    1.17  val rep_claset_of = rep_cs o claset_of;
    1.18  
     2.1 --- a/src/Pure/simplifier.ML	Wed Apr 10 17:17:16 2013 +0200
     2.2 +++ b/src/Pure/simplifier.ML	Wed Apr 10 17:27:38 2013 +0200
     2.3 @@ -10,7 +10,6 @@
     2.4    include BASIC_RAW_SIMPLIFIER
     2.5    val map_simpset: (simpset -> simpset) -> Proof.context -> Proof.context
     2.6    val simpset_of: Proof.context -> simpset
     2.7 -  val global_simpset_of: theory -> simpset
     2.8    val Addsimprocs: simproc list -> unit
     2.9    val Delsimprocs: simproc list -> unit
    2.10    val simp_tac: simpset -> int -> tactic
    2.11 @@ -169,8 +168,6 @@
    2.12  (* global simpset *)
    2.13  
    2.14  fun map_simpset_global f = Context.theory_map (map_ss f);
    2.15 -fun global_simpset_of thy =
    2.16 -  Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy));
    2.17  
    2.18  fun Addsimprocs args = Context.>> (map_ss (fn ss => ss addsimprocs args));
    2.19  fun Delsimprocs args = Context.>> (map_ss (fn ss => ss delsimprocs args));