# HG changeset patch # User wenzelm # Date 1129651171 -7200 # Node ID ff78ecd1e768eeede61851bf46ac52e7fcb3b612 # Parent 1733b4680fded5fd591c3229007357aee16e825f renamed set_context to context; data extend: reset context; diff -r 1733b4680fde -r ff78ecd1e768 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Tue Oct 18 17:59:30 2005 +0200 +++ b/src/Pure/simplifier.ML Tue Oct 18 17:59:31 2005 +0200 @@ -47,8 +47,9 @@ val clear_ss: simpset -> simpset val debug_bounds: bool ref val inherit_context: simpset -> simpset -> simpset - val the_context: simpset -> Context.proof - val set_context: Context.proof -> simpset -> simpset + val the_context: simpset -> Proof.context + val context: Proof.context -> simpset -> simpset + val theory_context: theory -> simpset -> simpset val simproc_i: theory -> string -> term list -> (theory -> simpset -> term -> thm option) -> simproc val simproc: theory -> string -> string list @@ -92,7 +93,7 @@ val empty = ref empty_ss; fun copy (ref ss) = ref ss: T; (*create new reference!*) - val extend = copy; + fun extend (ref ss) = ref (MetaSimplifier.inherit_context empty_ss ss); fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2)); fun print _ (ref ss) = print_ss ss; end); @@ -104,7 +105,7 @@ val change_simpset_of = change o GlobalSimpset.get; fun change_simpset f = change_simpset_of (Context.the_context ()) f; -fun simpset_of thy = MetaSimplifier.set_context (Context.init_proof thy) (get_simpset thy); +fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_simpset thy); val simpset = simpset_of o Context.the_context; @@ -134,7 +135,7 @@ val get_local_simpset = LocalSimpset.get; val put_local_simpset = LocalSimpset.put; -fun local_simpset_of ctxt = MetaSimplifier.set_context ctxt (get_local_simpset ctxt); +fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_local_simpset ctxt); (* attributes *)