# HG changeset patch # User wenzelm # Date 1169298557 -3600 # Node ID 0f26cd597193514d999296c4b97af8f289629289 # Parent fa8960e165a67bf5d0a735da16103a364c22e1ba added @{simpset}; diff -r fa8960e165a6 -r 0f26cd597193 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sat Jan 20 14:09:16 2007 +0100 +++ b/src/Pure/simplifier.ML Sat Jan 20 14:09:17 2007 +0100 @@ -138,6 +138,9 @@ fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_local_simpset ctxt); +val _ = ML_Context.value_antiq "simpset" + (Scan.succeed ("simpset", "Simplifier.local_simpset_of (ML_Context.the_local_context ())")); + (* attributes *)