# HG changeset patch
# User wenzelm
# Date 1365607036 -7200
# Node ID 3d8720271ebf614dee6f5125f1e60a28b685f173
# Parent  532e0ac5a66dd728b4cb6923403a27629ce755b7
discontinued obsolete ML antiquotation @{claset};

diff -r 532e0ac5a66d -r 3d8720271ebf src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Wed Apr 10 17:02:47 2013 +0200
+++ b/src/FOL/FOL.thy	Wed Apr 10 17:17:16 2013 +0200
@@ -181,24 +181,19 @@
 open Basic_Classical;
 *}
 
-setup {*
-  ML_Antiquote.value @{binding claset}
-    (Scan.succeed "Cla.claset_of ML_context")
-*}
-
 setup Cla.setup
 
 (*Propositional rules*)
 lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
   and [elim!] = conjE disjE impCE FalseE iffCE
-ML {* val prop_cs = @{claset} *}
+ML {* val prop_cs = claset_of @{context} *}
 
 (*Quantifier rules*)
 lemmas [intro!] = allI ex_ex1I
   and [intro] = exI
   and [elim!] = exE alt_ex1E
   and [elim] = allE
-ML {* val FOL_cs = @{claset} *}
+ML {* val FOL_cs = claset_of @{context} *}
 
 ML {*
   structure Blast = Blast
diff -r 532e0ac5a66d -r 3d8720271ebf 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)