# HG changeset patch
# User wenzelm
# Date 1214329394 -7200
# Node ID 2cd6c60cc10b849e4082b147396149f02f010f4b
# Parent  ed3719ffdf00758479e6f6fae10626b70505c56e
ML_Antiquote.value;

diff -r ed3719ffdf00 -r 2cd6c60cc10b src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Tue Jun 24 19:43:12 2008 +0200
+++ b/src/FOL/cladata.ML	Tue Jun 24 19:43:14 2008 +0200
@@ -22,8 +22,7 @@
 structure Cla = ClassicalFun(Classical_Data);
 structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
 
-ML_Context.value_antiq "claset"
-  (Scan.succeed ("claset", "Cla.local_claset_of (ML_Context.the_local_context ())"));
+ML_Antiquote.value "claset" (Scan.succeed "Cla.local_claset_of (ML_Context.the_local_context ())");
 
 
 (*Propositional rules*)
diff -r ed3719ffdf00 -r 2cd6c60cc10b src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Tue Jun 24 19:43:12 2008 +0200
+++ b/src/FOL/simpdata.ML	Tue Jun 24 19:43:14 2008 +0200
@@ -166,7 +166,7 @@
   val iffD1 = @{thm iffD1} val iffD2 = @{thm iffD2} val notE = @{thm notE});
 open Clasimp;
 
-ML_Context.value_antiq "clasimpset"
-  (Scan.succeed ("clasimpset", "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())"));
+ML_Antiquote.value "clasimpset"
+  (Scan.succeed "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())");
 
 val FOL_css = (FOL_cs, FOL_ss);
diff -r ed3719ffdf00 -r 2cd6c60cc10b src/HOL/HOL.thy
--- 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");
 
diff -r ed3719ffdf00 -r 2cd6c60cc10b src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Jun 24 19:43:12 2008 +0200
+++ b/src/HOL/simpdata.ML	Tue Jun 24 19:43:14 2008 +0200
@@ -160,8 +160,8 @@
   val iffD1 = @{thm iffD1} val iffD2 = @{thm iffD2} val notE = @{thm notE});
 open Clasimp;
 
-val _ = ML_Context.value_antiq "clasimpset"
-  (Scan.succeed ("clasimpset", "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())"));
+val _ = ML_Antiquote.value "clasimpset"
+  (Scan.succeed "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())");
 
 val mksimps_pairs =
   [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),
diff -r ed3719ffdf00 -r 2cd6c60cc10b src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Tue Jun 24 19:43:12 2008 +0200
+++ b/src/Pure/simplifier.ML	Tue Jun 24 19:43:14 2008 +0200
@@ -133,8 +133,8 @@
 
 fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt));
 
-val _ = ML_Context.value_antiq "simpset"
-  (Scan.succeed ("simpset", "Simplifier.local_simpset_of (ML_Context.the_local_context ())"));
+val _ = ML_Antiquote.value "simpset"
+  (Scan.succeed "Simplifier.local_simpset_of (ML_Context.the_local_context ())");
 
 
 
@@ -167,9 +167,8 @@
     | NONE => error ("Undefined simplification procedure: " ^ quote name))
   end;
 
-val _ = ML_Context.value_antiq "simproc" (Scan.lift Args.name >> (fn name =>
-  ("simproc",
-    "Simplifier.get_simproc (ML_Context.the_generic_context ()) " ^ ML_Syntax.print_string name)));
+val _ = ML_Antiquote.value "simproc" (Scan.lift Args.name >> (fn name =>
+  "Simplifier.get_simproc (ML_Context.the_generic_context ()) " ^ ML_Syntax.print_string name));
 
 
 (* define simprocs *)