--- 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*)
--- 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);
--- 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");
--- 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}]),
--- 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 *)