--- a/src/HOL/HOL.thy Tue Jun 24 19:43:12 2008 +0200
+++ b/src/HOL/HOL.thy Tue Jun 24 19:43:14 2008 +0200
@@ -934,8 +934,8 @@
structure BasicClassical: BASIC_CLASSICAL = Classical;
open BasicClassical;
-ML_Context.value_antiq "claset"
- (Scan.succeed ("claset", "Classical.local_claset_of (ML_Context.the_local_context ())"));
+ML_Antiquote.value "claset"
+ (Scan.succeed "Classical.local_claset_of (ML_Context.the_local_context ())");
structure ResAtpset = NamedThmsFun(val name = "atp" val description = "ATP rules");