# HG changeset patch
# User wenzelm
# Date 1288300792 -7200
# Node ID 56fad09655a5079ca1b0ace201b01830066125c6
# Parent  a2dde53b15efa90c47b5d6191321183815894000
discontinued obsolete ML antiquotation @{theory_ref};

diff -r a2dde53b15ef -r 56fad09655a5 NEWS
--- a/NEWS	Thu Oct 28 22:59:33 2010 +0200
+++ b/NEWS	Thu Oct 28 23:19:52 2010 +0200
@@ -339,6 +339,10 @@
 Fail if the argument is false.  Due to inlining the source position of
 failed assertions is included in the error output.
 
+* Discontinued antiquotation @{theory_ref}, which is obsolete since ML
+text is in practice always evaluated with a stable theory checkpoint.
+Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.
+
 * Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
 meaning.
 
diff -r a2dde53b15ef -r 56fad09655a5 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Thu Oct 28 22:59:33 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Thu Oct 28 23:19:52 2010 +0200
@@ -226,11 +226,10 @@
 text %mlantiq {*
   \begin{matharray}{rcl}
   @{ML_antiquotation_def "theory"} & : & @{text ML_antiquotation} \\
-  @{ML_antiquotation_def "theory_ref"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
   \begin{rail}
-  ('theory' | 'theory\_ref') nameref?
+  'theory' nameref?
   ;
   \end{rail}
 
@@ -243,10 +242,6 @@
   theory @{text "A"} of the background theory of the current context
   --- as abstract value.
 
-  \item @{text "@{theory_ref}"} is similar to @{text "@{theory}"}, but
-  produces a @{ML_type theory_ref} via @{ML "Theory.check_thy"} as
-  explained above.
-
   \end{description}
 *}
 
diff -r a2dde53b15ef -r 56fad09655a5 doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Thu Oct 28 22:59:33 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Thu Oct 28 23:19:52 2010 +0200
@@ -262,11 +262,10 @@
 \begin{isamarkuptext}%
 \begin{matharray}{rcl}
   \indexdef{}{ML antiquotation}{theory}\hypertarget{ML antiquotation.theory}{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
-  \indexdef{}{ML antiquotation}{theory\_ref}\hypertarget{ML antiquotation.theory-ref}{\hyperlink{ML antiquotation.theory-ref}{\mbox{\isa{theory{\isacharunderscore}ref}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
   \end{matharray}
 
   \begin{rail}
-  ('theory' | 'theory\_ref') nameref?
+  'theory' nameref?
   ;
   \end{rail}
 
@@ -279,10 +278,6 @@
   theory \isa{A} of the background theory of the current context
   --- as abstract value.
 
-  \item \isa{{\isacharat}{\isacharbraceleft}theory{\isacharunderscore}ref{\isacharbraceright}} is similar to \isa{{\isacharat}{\isacharbraceleft}theory{\isacharbraceright}}, but
-  produces a \verb|theory_ref| via \verb|Theory.check_thy| as
-  explained above.
-
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
diff -r a2dde53b15ef -r 56fad09655a5 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Thu Oct 28 22:59:33 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Thu Oct 28 23:19:52 2010 +0200
@@ -71,12 +71,6 @@
     "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
   || Scan.succeed "ML_Context.the_global_context ()");
 
-val _ = value "theory_ref"
-  (Scan.lift Args.name >> (fn name =>
-    "Theory.check_thy (Context.get_theory (ML_Context.the_global_context ()) " ^
-      ML_Syntax.print_string name ^ ")")
-  || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
-
 val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
 
 val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
diff -r a2dde53b15ef -r 56fad09655a5 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Thu Oct 28 22:59:33 2010 +0200
+++ b/src/ZF/simpdata.ML	Thu Oct 28 23:19:52 2010 +0200
@@ -59,10 +59,10 @@
 
 in
 
-val defBEX_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
+val defBEX_regroup = Simplifier.simproc_global @{theory}
   "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
 
-val defBALL_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
+val defBALL_regroup = Simplifier.simproc_global @{theory}
   "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
 
 end;