1.1 --- a/src/Pure/simplifier.ML	Sat Jan 20 14:09:16 2007 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Sat Jan 20 14:09:17 2007 +0100
     1.3 @@ -138,6 +138,9 @@
     1.4  
     1.5  fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_local_simpset ctxt);
     1.6  
     1.7 +val _ = ML_Context.value_antiq "simpset"
     1.8 +  (Scan.succeed ("simpset", "Simplifier.local_simpset_of (ML_Context.the_local_context ())"));
     1.9 +
    1.10  
    1.11  (* attributes *)
    1.12