src/FOL/simpdata.ML

--- a/src/FOL/simpdata.ML	Sat Jan 20 14:09:10 2007 +0100
+++ b/src/FOL/simpdata.ML	Sat Jan 20 14:09:11 2007 +0100
@@ -342,4 +342,7 @@
   val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE);
 open Clasimp;
 
+ML_Context.value_antiq "clasimpset"
+  (Scan.succeed ("clasimpset", "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())"));
+
 val FOL_css = (FOL_cs, FOL_ss);