# HG changeset patch
# User wenzelm
# Date 1214329401 -7200
# Node ID 21719887bd234f44246a512bd5761df510feda5c
# Parent  d44490b0619004b0a9306883f9338ab535ec3a0e
moved concrete antiquotations to ml_antiquote.ML;

diff -r d44490b06190 -r 21719887bd23 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Jun 24 19:43:20 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Jun 24 19:43:21 2008 +0200
@@ -185,17 +185,6 @@
   if Context.theory_name thy = name then thy
   else get_theory name;
 
-val _ = ML_Context.value_antiq "theory"
-  (Scan.lift Args.name
-    >> (fn name => (name ^ "_thy", "ThyInfo.get_theory " ^ ML_Syntax.print_string name))
-  || Scan.succeed ("thy", "ML_Context.the_global_context ()"));
-
-val _ = ML_Context.value_antiq "theory_ref"
-  (Scan.lift Args.name
-    >> (fn name => (name ^ "_thy",
-        "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")"))
-  || Scan.succeed ("thy", "Theory.check_thy (ML_Context.the_global_context ())"));
-
 
 
 (** thy operations **)