# 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 *)