moved concrete antiquotations to ml_antiquote.ML;
authorwenzelm
Tue, 24 Jun 2008 19:43:21 +0200
changeset 27345 21719887bd23
parent 27344 d44490b06190
child 27346 b664e5bc95fd
moved concrete antiquotations to ml_antiquote.ML;
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 **)