src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Wed Apr 10 17:02:47 2013 +0200
+++ b/src/HOL/HOL.thy	Wed Apr 10 17:17:16 2013 +0200
@@ -843,11 +843,6 @@
 open Basic_Classical;
 *}
 
-setup {*
-  ML_Antiquote.value @{binding claset}
-    (Scan.succeed "Classical.claset_of ML_context")
-*}
-
 setup Classical.setup
 
 setup {*
@@ -888,7 +883,7 @@
 declare exE [elim!]
   allE [elim]
 
-ML {* val HOL_cs = @{claset} *}
+ML {* val HOL_cs = claset_of @{context} *}
 
 lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
   apply (erule swap)