src/HOL/simpdata.ML
changeset 27338 2cd6c60cc10b
parent 26711 3a478bfa1650
child 28262 aa7ca36d67fd
--- 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}]),