# HG changeset patch
# User wenzelm
# Date 1169298551 -3600
# Node ID cdd92316dd316fd12c411801e4618a888b30fd20
# Parent  025dfa637f783a145c5507f3d64aa9d8bc05869c
added @{clasimpset};

diff -r 025dfa637f78 -r cdd92316dd31 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);
diff -r 025dfa637f78 -r cdd92316dd31 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Sat Jan 20 14:09:10 2007 +0100
+++ b/src/HOL/simpdata.ML	Sat Jan 20 14:09:11 2007 +0100
@@ -177,9 +177,12 @@
 structure Clasimp = ClasimpFun
  (structure Simplifier = Simplifier and Splitter = Splitter
   and Classical  = Classical and Blast = Blast
-  val iffD1 = thm "iffD1" val iffD2 = thm "iffD2" val notE = thm "notE")
+  val iffD1 = thm "iffD1" val iffD2 = thm "iffD2" val notE = thm "notE");
 open Clasimp;
 
+val _ = ML_Context.value_antiq "clasimpset"
+  (Scan.succeed ("clasimpset", "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())"));
+
 val mksimps_pairs =
   [("op -->", [thm "mp"]), ("op &", [thm "conjunct1", thm "conjunct2"]),
    ("All", [thm "spec"]), ("True", []), ("False", []),