--- a/src/HOL/simpdata.ML Tue Jun 24 19:43:12 2008 +0200
+++ b/src/HOL/simpdata.ML Tue Jun 24 19:43:14 2008 +0200
@@ -160,8 +160,8 @@
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 _ = ML_Antiquote.value "clasimpset"
+ (Scan.succeed "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())");
val mksimps_pairs =
[("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),