Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ML_Antiquote.value;
authorwenzelm
Tue, 24 Jun 2008 19:43:14 +0200
changeset 27338 2cd6c60cc10b
parent 27337 ed3719ffdf00
child 27339 07194f87f9d0
ML_Antiquote.value;
src/FOL/cladata.ML file | annotate | diff | comparison | revisions
src/FOL/simpdata.ML file | annotate | diff | comparison | revisions
src/HOL/HOL.thy file | annotate | diff | comparison | revisions
src/HOL/simpdata.ML file | annotate | diff | comparison | revisions
src/Pure/simplifier.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle