src/HOL/HOL.thy
changeset 32149 ef59550a55d3
parent 32119 a853099fd9ca
child 32171 220abde9962b
--- a/src/HOL/HOL.thy	Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/HOL.thy	Thu Jul 23 18:44:09 2009 +0200
@@ -833,7 +833,7 @@
 open BasicClassical;
 
 ML_Antiquote.value "claset"
-  (Scan.succeed "Classical.local_claset_of (ML_Context.the_local_context ())");
+  (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())");
 
 structure ResAtpset = Named_Thms
   (val name = "atp" val description = "ATP rules");