1.1 --- a/src/Pure/simplifier.ML	Fri Mar 20 17:04:44 2009 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Fri Mar 20 17:12:37 2009 +0100
     1.3 @@ -10,15 +10,8 @@
     1.4    include BASIC_META_SIMPLIFIER
     1.5    val change_simpset: (simpset -> simpset) -> unit
     1.6    val simpset_of: theory -> simpset
     1.7 -  val simpset: unit -> simpset
     1.8 -  val SIMPSET: (simpset -> tactic) -> tactic
     1.9 -  val SIMPSET': (simpset -> 'a -> tactic) -> 'a -> tactic
    1.10 -  val Addsimps: thm list -> unit
    1.11 -  val Delsimps: thm list -> unit
    1.12    val Addsimprocs: simproc list -> unit
    1.13    val Delsimprocs: simproc list -> unit
    1.14 -  val Addcongs: thm list -> unit
    1.15 -  val Delcongs: thm list -> unit
    1.16    val local_simpset_of: Proof.context -> simpset
    1.17    val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
    1.18    val safe_asm_full_simp_tac: simpset -> int -> tactic
    1.19 @@ -27,11 +20,6 @@
    1.20    val          full_simp_tac: simpset -> int -> tactic
    1.21    val        asm_lr_simp_tac: simpset -> int -> tactic
    1.22    val      asm_full_simp_tac: simpset -> int -> tactic
    1.23 -  val               Simp_tac:            int -> tactic
    1.24 -  val           Asm_simp_tac:            int -> tactic
    1.25 -  val          Full_simp_tac:            int -> tactic
    1.26 -  val        Asm_lr_simp_tac:            int -> tactic
    1.27 -  val      Asm_full_simp_tac:            int -> tactic
    1.28    val          simplify: simpset -> thm -> thm
    1.29    val      asm_simplify: simpset -> thm -> thm
    1.30    val     full_simplify: simpset -> thm -> thm
    1.31 @@ -138,17 +126,9 @@
    1.32  fun map_simpset f = Context.theory_map (map_ss f);
    1.33  fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
    1.34  fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
    1.35 -val simpset = simpset_of o ML_Context.the_global_context;
    1.36  
    1.37 -fun SIMPSET tacf st = tacf (simpset_of (Thm.theory_of_thm st)) st;
    1.38 -fun SIMPSET' tacf i st = tacf (simpset_of (Thm.theory_of_thm st)) i st;
    1.39 -
    1.40 -fun Addsimps args = change_simpset (fn ss => ss addsimps args);
    1.41 -fun Delsimps args = change_simpset (fn ss => ss delsimps args);
    1.42  fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
    1.43  fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
    1.44 -fun Addcongs args = change_simpset (fn ss => ss addcongs args);
    1.45 -fun Delcongs args = change_simpset (fn ss => ss delcongs args);
    1.46  
    1.47  
    1.48  (* local simpset *)
    1.49 @@ -283,13 +263,6 @@
    1.50  val asm_full_simp_tac = generic_simp_tac false (true, true, true);
    1.51  val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
    1.52  
    1.53 -(*the abstraction over the proof state delays the dereferencing*)
    1.54 -fun          Simp_tac i st =          simp_tac (simpset ()) i st;
    1.55 -fun      Asm_simp_tac i st =      asm_simp_tac (simpset ()) i st;
    1.56 -fun     Full_simp_tac i st =     full_simp_tac (simpset ()) i st;
    1.57 -fun   Asm_lr_simp_tac i st =   asm_lr_simp_tac (simpset ()) i st;
    1.58 -fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
    1.59 -
    1.60  
    1.61  (* conversions *)
    1.62