src/HOL/HOL.thy
changeset 27338 2cd6c60cc10b
parent 27326 d3beec370964
child 27572 67cd6ed76446
     1.1 --- a/src/HOL/HOL.thy	Tue Jun 24 19:43:12 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Jun 24 19:43:14 2008 +0200
     1.3 @@ -934,8 +934,8 @@
     1.4  structure BasicClassical: BASIC_CLASSICAL = Classical; 
     1.5  open BasicClassical;
     1.6  
     1.7 -ML_Context.value_antiq "claset"
     1.8 -  (Scan.succeed ("claset", "Classical.local_claset_of (ML_Context.the_local_context ())"));
     1.9 +ML_Antiquote.value "claset"
    1.10 +  (Scan.succeed "Classical.local_claset_of (ML_Context.the_local_context ())");
    1.11  
    1.12  structure ResAtpset = NamedThmsFun(val name = "atp" val description = "ATP rules");
    1.13