src/Pure/simplifier.ML
changeset 17898 ff78ecd1e768
parent 17883 efa1bc2bdcc6
child 17967 7a733b7438e1
     1.1 --- a/src/Pure/simplifier.ML	Tue Oct 18 17:59:30 2005 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Tue Oct 18 17:59:31 2005 +0200
     1.3 @@ -47,8 +47,9 @@
     1.4    val clear_ss: simpset -> simpset
     1.5    val debug_bounds: bool ref
     1.6    val inherit_context: simpset -> simpset -> simpset
     1.7 -  val the_context: simpset -> Context.proof
     1.8 -  val set_context: Context.proof -> simpset -> simpset
     1.9 +  val the_context: simpset -> Proof.context
    1.10 +  val context: Proof.context -> simpset -> simpset
    1.11 +  val theory_context: theory  -> simpset -> simpset
    1.12    val simproc_i: theory -> string -> term list
    1.13      -> (theory -> simpset -> term -> thm option) -> simproc
    1.14    val simproc: theory -> string -> string list
    1.15 @@ -92,7 +93,7 @@
    1.16  
    1.17    val empty = ref empty_ss;
    1.18    fun copy (ref ss) = ref ss: T;            (*create new reference!*)
    1.19 -  val extend = copy;
    1.20 +  fun extend (ref ss) = ref (MetaSimplifier.inherit_context empty_ss ss);
    1.21    fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
    1.22    fun print _ (ref ss) = print_ss ss;
    1.23  end);
    1.24 @@ -104,7 +105,7 @@
    1.25  val change_simpset_of = change o GlobalSimpset.get;
    1.26  fun change_simpset f = change_simpset_of (Context.the_context ()) f;
    1.27  
    1.28 -fun simpset_of thy = MetaSimplifier.set_context (Context.init_proof thy) (get_simpset thy);
    1.29 +fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_simpset thy);
    1.30  val simpset = simpset_of o Context.the_context;
    1.31  
    1.32  
    1.33 @@ -134,7 +135,7 @@
    1.34  val get_local_simpset = LocalSimpset.get;
    1.35  val put_local_simpset = LocalSimpset.put;
    1.36  
    1.37 -fun local_simpset_of ctxt = MetaSimplifier.set_context ctxt (get_local_simpset ctxt);
    1.38 +fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_local_simpset ctxt);
    1.39  
    1.40  
    1.41  (* attributes *)